ProperSpace

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

Statistics

Metric	Count
Definitions	0
Theorems tangentConeAt_nonempty_of_properSpace	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tangentConeAt_nonempty_of_properSpace 📖	mathematical	—	Set.Nonempty Set Set.instInter tangentConeAt NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Compl.compl Set.instCompl Set.instSingletonSet NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace accPt_iff_nhds Metric.closedBall_mem_nhds add_sub_cancel NormedField.exists_one_lt_norm rescale_to_shell zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero AddLeftCancelSemigroup.toIsLeftCancelAdd IsCompact.tendsto_subseq IsCompact.diff ProperSpace.isCompact_closedBall Metric.isOpen_ball dist_zero_right LT.lt.le mem_tangentConeAt_of_seq Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp squeeze_zero_norm dist_eq_norm StrictMono.tendsto_atTop Filter.Eventually.of_forall Mathlib.Tactic.Contrapose.contrapose₃ one_div dist_self norm_zero

---

← Back to Index