DimOne

📁 Source: Mathlib/Analysis/Calculus/TangentCone/DimOne.lean

Statistics

Metric	Count
Definitions	0
Theorems uniqueDiffWithinAt, tangentConeAt_eq_univ, uniqueDiffWithinAt_iff_accPt	3
Total	3

AccPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniqueDiffWithinAt 📖	mathematical	—	UniqueDiffWithinAt DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	uniqueDiffWithinAt_iff_accPt

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tangentConeAt_eq_univ 📖	mathematical	—	tangentConeAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Set.univ	—	Set.eq_univ_of_forall mem_tangentConeAt_of_frequently Filter.Tendsto.mono_left Continuous.tendsto' Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_id' continuous_const sub_self inf_le_left add_sub_cancel tendsto_nhds_of_eventually_eq Filter.Eventually.mono eventually_mem_nhdsWithin div_mul_cancel₀
uniqueDiffWithinAt_iff_accPt 📖	mathematical	—	UniqueDiffWithinAt DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing AccPt Filter.principal	—	UniqueDiffWithinAt.accPt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsSimpleRing.instNontrivial DivisionRing.isSimpleRing tangentConeAt_eq_univ Submodule.span_univ mem_closure_iff_clusterPt AccPt.clusterPt

---

← Back to Index