Real

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

Statistics

Metric	Count
Definitions	0
Theorems span_tangentConeAt, mem_tangentConeAt_of_openSegment_subset, mem_tangentConeAt_of_segment_subset, sub_mem_posTangentConeAt_of_openSegment_subset, uniqueDiffOn_Icc, uniqueDiffOn_Icc_zero_one, uniqueDiffOn_Ici, uniqueDiffOn_Ico, uniqueDiffOn_Iic, uniqueDiffOn_Iio, uniqueDiffOn_Ioc, uniqueDiffOn_Ioi, uniqueDiffOn_Ioo, uniqueDiffOn_convex, uniqueDiffWithinAt_Ici, uniqueDiffWithinAt_Iic, uniqueDiffWithinAt_Iio, uniqueDiffWithinAt_Ioi, uniqueDiffWithinAt_Ioo, uniqueDiffWithinAt_convex	20
Total	20

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
span_tangentConeAt 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.Nonempty interior Set Set.instMembership closure	Submodule.span Real Real.semiring AddCommGroup.toAddCommMonoid tangentConeAt SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Top.top Submodule Submodule.instTop	—	mem_interior_iff_mem_nhds IsOpen.mem_nhds isOpen_interior Filter.mem_of_superset IsOpenMap.image_mem_nhds isOpenMap_sub_right mem_tangentConeAt_of_openSegment_subset Set.Subset.trans openSegment_closure_interior_subset_interior ContinuousSMul.continuousConstSMul interior_subset Submodule.eq_top_of_nonempty_interior' IsTopologicalAddGroup.toContinuousAdd NormedField.nhdsWithin_isUnit_neBot interior_mono Submodule.subset_span

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_tangentConeAt_of_openSegment_subset 📖	mathematical	Set Set.instHasSubset openSegment Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set Set.instMembership tangentConeAt Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SubNegMonoid.toSub	—	tangentConeAt_mono_field NNReal.instIsScalarTowerOfReal IsScalarTower.left sub_mem_posTangentConeAt_of_openSegment_subset
mem_tangentConeAt_of_segment_subset 📖	mathematical	Set Set.instHasSubset segment Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set Set.instMembership tangentConeAt Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid SubNegMonoid.toSub	—	mem_tangentConeAt_of_openSegment_subset HasSubset.Subset.trans Set.instIsTransSubset openSegment_subset_segment
sub_mem_posTangentConeAt_of_openSegment_subset 📖	mathematical	Set Set.instHasSubset openSegment Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	Set Set.instMembership tangentConeAt NNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring AddCommGroup.toAddCommMonoid SubNegMonoid.toSub	—	mem_tangentConeAt_of_add_smul_mem NNReal.instContinuousSMulOfReal nhdsGT_neBot NNReal.instOrderTopology IsStrictOrderedRing.toNoMaxOrder Filter.tendsto_id' nhdsGT_le_nhdsNE Filter.mp_mem Ioo_mem_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology one_pos LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Filter.univ_mem' openSegment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_zero Nat.cast_one add_comm
uniqueDiffOn_Icc 📖	mathematical	Real Real.instLT	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder	—	uniqueDiffOn_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Icc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
uniqueDiffOn_Icc_zero_one 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Real.instZero Real.instOne	—	uniqueDiffOn_Icc zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
uniqueDiffOn_Ici 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder	—	uniqueDiffOn_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Ici Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
uniqueDiffOn_Ico 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ico Real.instPreorder	—	uniqueDiffOn_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Ico Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Ico instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Set.Ico_eq_empty
uniqueDiffOn_Iic 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iic Real.instPreorder	—	uniqueDiffOn_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Iic Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMinOrderOfNontrivial
uniqueDiffOn_Iio 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iio Real.instPreorder	—	IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal
uniqueDiffOn_Ioc 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioc Real.instPreorder	—	uniqueDiffOn_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Ioc Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Ioc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Set.Ioc_eq_empty
uniqueDiffOn_Ioi 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder	—	IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing isOpen_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal
uniqueDiffOn_Ioo 📖	mathematical	—	UniqueDiffOn Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioo Real.instPreorder	—	IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing isOpen_Ioo OrderTopology.to_orderClosedTopology instOrderTopologyReal
uniqueDiffOn_convex 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.Nonempty interior	UniqueDiffOn Real Real.semiring	—	uniqueDiffWithinAt_convex subset_closure
uniqueDiffWithinAt_Ici 📖	mathematical	—	UniqueDiffWithinAt Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder	—	UniqueDiffWithinAt.mono uniqueDiffWithinAt_Ioi Set.Ioi_subset_Ici_self
uniqueDiffWithinAt_Iic 📖	mathematical	—	UniqueDiffWithinAt Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iic Real.instPreorder	—	UniqueDiffWithinAt.mono uniqueDiffWithinAt_Iio Set.Iio_subset_Iic_self
uniqueDiffWithinAt_Iio 📖	mathematical	—	UniqueDiffWithinAt Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iio Real.instPreorder	—	uniqueDiffWithinAt_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Iio Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_Iio LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instReflLe
uniqueDiffWithinAt_Ioi 📖	mathematical	—	UniqueDiffWithinAt Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder	—	uniqueDiffWithinAt_convex ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIsTopologicalAddGroupReal convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_Ioi LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instReflLe
uniqueDiffWithinAt_Ioo 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder	UniqueDiffWithinAt Real Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioo Real.instPreorder	—	IsOpen.uniqueDiffWithinAt NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing isOpen_Ioo OrderTopology.to_orderClosedTopology instOrderTopologyReal
uniqueDiffWithinAt_convex 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.Nonempty interior Set Set.instMembership closure	UniqueDiffWithinAt Real Real.semiring	—	Convex.span_tangentConeAt

---

← Back to Index