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 tangentConeAt 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.instMembership tangentConeAt 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.instMembership tangentConeAt 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.instMembership tangentConeAt NNReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal SubNegMonoid.toSub	—	mem_tangentConeAt_of_add_smul_mem NNReal.instContinuousSMulOfReal nhdsGT_neBot NNReal.instOrderTopology NNReal.instDenselyOrdered IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing 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.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 IsTopologicalSemiring.toContinuousAdd 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 IsTopologicalSemiring.toContinuousAdd 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 IsTopologicalSemiring.toContinuousAdd 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	—	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
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
uniqueDiffWithinAt_Ioo 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder	UniqueDiffWithinAt Real.semiring Real.instAddCommGroup Semiring.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	IsOpen.uniqueDiffWithinAt NormedField.nhdsNE_neBot ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd 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	—	Convex.span_tangentConeAt

---

← Back to Index