Topology

📁 Source: Mathlib/Analysis/Convex/Topology.lean

Statistics

Metric	Count
Definitions closedConvexHull	1
Theorems Ioo_subset_of_mem_closure, add_smul_mem_interior, add_smul_mem_interior', add_smul_sub_mem_interior, add_smul_sub_mem_interior', closure, closure_interior_eq_closure_of_nonempty_interior, closure_subset_image_homothety_interior_of_one_lt, closure_subset_interior_image_homothety_of_one_lt, combo_closure_interior_mem_interior, combo_closure_interior_subset_interior, combo_interior_closure_mem_interior, combo_interior_closure_subset_interior, combo_interior_self_mem_interior, combo_interior_self_subset_interior, combo_self_interior_mem_interior, combo_self_interior_subset_interior, diff_singleton_eventually_mem_nhds, interior, interior_closure_eq_interior_of_nonempty_interior, nhdsWithin_diff_eq_nhdsGT, nhdsWithin_diff_eq_nhdsLT, nhdsWithin_diff_eq_nhdsNE, nhdsWithin_inter_Iio_eq_nhdsLT, nhdsWithin_inter_Ioi_eq_nhdsGT, nontrivial_iff_nonempty_interior, openSegment_closure_interior_subset_interior, openSegment_interior_closure_subset_interior, openSegment_interior_self_subset_interior, openSegment_self_interior_subset_interior, strictConvex, strictConvex', subset_interior_image_homothety_of_one_lt, convex, ball_eq_openSegment, closedBall_eq_segment, convex_iff_isPreconnected, isClosed_convexHull, isCompact_convexHull, closedConvexHull_closure_eq_closedConvexHull, closedConvexHull_eq_closure_convexHull, closedConvexHull_isClosed, closedConvexHull_min, closure_openSegment, closure_subset_closedConvexHull, convexHull_subset_closedConvexHull, convex_closedConvexHull, convex_closed_sInter, isClosed_closedConvexHull, segment_subset_closure_openSegment, subset_closedConvexHull	51
Total	52

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ioo_subset_of_mem_closure 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure	Set.instHasSubset Set.Ioo PartialOrder.toPreorder	—	subsingleton_or_nontrivial Set.Subsingleton.closure T5Space.toT1Space OrderTopology.t5Space Set.Ioo_eq_empty interior_Ioo OrderTopology.to_orderClosedTopology interior_mono Ioo_subset_openSegment openSegment_subset closure LinearOrderedAddCommGroup.toIsTopologicalAddGroup IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing interior_closure_eq_interior_of_nonempty_interior ContinuousMul.to_continuousSMul nontrivial_iff_nonempty_interior interior_subset
add_smul_mem_interior 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	—	add_smul_mem_interior' subset_closure
add_smul_mem_interior' 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership closure interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	—	add_sub_cancel_left add_smul_sub_mem_interior'
add_smul_sub_mem_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub	—	add_smul_sub_mem_interior' subset_closure
add_smul_sub_mem_interior' 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership closure interior Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub	—	smul_sub add_sub sub_smul one_smul add_comm combo_interior_closure_mem_interior sub_nonneg add_sub_cancel
closure 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	closure	—	Continuous.add IsTopologicalAddGroup.toContinuousAdd Continuous.const_smul continuous_fst continuous_snd map_mem_closure₂
closure_interior_eq_closure_of_nonempty_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Nonempty interior	closure	—	subset_antisymm Set.instAntisymmSubset closure_mono interior_subset openSegment_interior_closure_subset_interior ContinuousSMul.continuousConstSMul segment_subset_closure_openSegment LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsTopologicalAddGroup.toContinuousAdd right_mem_segment IsStrictOrderedRing.toZeroLEOneClass
closure_subset_image_homothety_interior_of_one_lt 📖	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 Set.instMembership interior Real.instLT Real.instOne	Set.instHasSubset closure Set.image DFunLike.coe AffineMap CommRing.toRing Real.commRing addGroupIsAddTorsor AffineMap.instFunLike AffineMap.homothety	—	LT.lt.ne' LT.lt.trans one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing openSegment_interior_closure_subset_interior ContinuousSMul.continuousConstSMul openSegment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inv_one Set.inv_Ioi₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zero_lt_one' Set.image_inv_eq_inv Set.image_image AffineMap.homothety_eq_lineMap Set.mem_image_of_mem AffineEquiv.apply_symm_apply
closure_subset_interior_image_homothety_of_one_lt 📖	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 Set.instMembership interior Real.instLT Real.instOne	Set.instHasSubset closure Set.image DFunLike.coe AffineMap CommRing.toRing Real.commRing addGroupIsAddTorsor AffineMap.instFunLike AffineMap.homothety	—	HasSubset.Subset.trans Set.instIsTransSubset closure_subset_image_homothety_interior_of_one_lt IsOpenMap.image_interior_subset AffineMap.homothety_isOpenMap instIsTopologicalAddTorsor ContinuousSMul.continuousConstSMul LT.lt.ne' LT.lt.trans one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
combo_closure_interior_mem_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership closure interior Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	combo_closure_interior_subset_interior Set.add_mem_add Set.smul_mem_smul_set
combo_closure_interior_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.smulSet closure interior	—	add_comm combo_interior_closure_subset_interior
combo_interior_closure_mem_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior closure Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	combo_interior_closure_subset_interior Set.add_mem_add Set.smul_mem_smul_set
combo_interior_closure_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.smulSet interior closure	—	Set.add_subset_add Set.Subset.rfl smul_closure_subset IsOpen.add_closure isOpen_interior subset_interior_add_left ContinuousConstVAdd.op VAddCommClass.continuousConstVAdd vaddCommClass_self IsTopologicalAddGroup.toContinuousAdd AddCommSemigroup.isCentralVAdd interior_mono set_combo_subset LT.lt.le interior_smul₀ LT.lt.ne'
combo_interior_self_mem_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	combo_interior_closure_mem_interior subset_closure
combo_interior_self_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.smulSet interior	—	Set.add_subset_add Set.Subset.rfl Set.image_mono subset_closure combo_interior_closure_subset_interior
combo_self_interior_mem_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	combo_closure_interior_mem_interior subset_closure
combo_self_interior_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Set Set.instHasSubset Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.smulSet interior	—	add_comm combo_interior_self_subset_interior
diff_singleton_eventually_mem_nhds 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	Filter.Eventually Set Filter Filter.instMembership nhds Set.instSDiff Set.instSingletonSet nhdsWithin	—	Filter.eq_or_neBot Filter.eventually_bot closure_mono Set.diff_subset mem_closure_iff_nhdsWithin_neBot Set.diff_eq Set.Iio_union_Ioi Set.inter_union_distrib_left nhdsWithin_union Filter.eventually_sup Ioo_subset_of_mem_closure instOrderTopologyOrderDual
interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	interior	—	convex_iff_openSegment_subset openSegment_closure_interior_subset_interior interior_subset_closure
interior_closure_eq_interior_of_nonempty_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Nonempty interior	closure	—	subset_antisymm Set.instAntisymmSubset AffineMap.lineMap_apply_one Filter.Eventually.exists_gt nhdsGT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Filter.Tendsto.eventually_mem Continuous.tendsto' AffineMap.lineMap_continuous instIsTopologicalAddTorsor mem_interior_iff_mem_nhds openSegment_interior_closure_subset_interior ContinuousSMul.continuousConstSMul AffineMap.lineMap_apply_zero image_openSegment covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Ioo_subset_openSegment zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one interior_mono subset_closure
nhdsWithin_diff_eq_nhdsGT 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure Set.instInter Set.Iio PartialOrder.toPreorder Set.instEmptyCollection Set.Nonempty Set.Ioi	nhdsWithin Set.instSDiff Set.instSingletonSet	—	Set.diff_eq Set.Iio_union_Ioi Set.inter_union_distrib_left nhdsWithin_union nhdsWithin_empty nhdsWithin_inter_Ioi_eq_nhdsGT sup_of_le_right
nhdsWithin_diff_eq_nhdsLT 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure Set.Nonempty Set.instInter Set.Iio PartialOrder.toPreorder Set.Ioi Set.instEmptyCollection	nhdsWithin Set.instSDiff Set.instSingletonSet	—	Set.diff_eq Set.Iio_union_Ioi Set.inter_union_distrib_left nhdsWithin_union nhdsWithin_inter_Iio_eq_nhdsLT nhdsWithin_empty sup_of_le_left
nhdsWithin_diff_eq_nhdsNE 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure Set.Nonempty Set.instInter Set.Iio PartialOrder.toPreorder Set.Ioi	nhdsWithin Set.instSDiff Set.instSingletonSet Compl.compl Set.instCompl	—	Set.diff_eq Set.Iio_union_Ioi Set.inter_union_distrib_left nhdsWithin_union nhdsWithin_inter_Iio_eq_nhdsLT nhdsWithin_inter_Ioi_eq_nhdsGT
nhdsWithin_inter_Iio_eq_nhdsLT 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure Set.Nonempty Set.instInter Set.Iio PartialOrder.toPreorder	nhdsWithin	—	nhdsWithin_inter_of_mem mem_nhdsLT_iff_exists_Ioo_subset instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Ioo_subset_of_mem_closure subset_closure
nhdsWithin_inter_Ioi_eq_nhdsGT 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instMembership closure Set.Nonempty Set.instInter Set.Ioi PartialOrder.toPreorder	nhdsWithin	—	nhdsWithin_inter_of_mem mem_nhdsGT_iff_exists_Ioo_subset instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Ioo_subset_of_mem_closure subset_closure
nontrivial_iff_nonempty_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	Set.Nontrivial Set.Nonempty interior	—	Set.Nonempty.mono interior_mono segment_subset inf_lt_sup Set.nonempty_Ioo LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono interior_Icc instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero instNoMaxOrderOfNontrivial segment_eq_Icc' Set.eq_singleton_or_nontrivial interior_subset interior_singleton instNeBotNhdsWithinComplSetSingletonOfNontrivial
openSegment_closure_interior_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership closure interior	Set.instHasSubset openSegment	—	combo_closure_interior_mem_interior LT.lt.le
openSegment_interior_closure_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior closure	Set.instHasSubset openSegment	—	combo_interior_closure_mem_interior LT.lt.le
openSegment_interior_self_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior	Set.instHasSubset openSegment	—	openSegment_interior_closure_subset_interior subset_closure
openSegment_self_interior_subset_interior 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership interior	Set.instHasSubset openSegment	—	openSegment_closure_interior_subset_interior subset_closure
strictConvex 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Pairwise Set Set.instSDiff interior Set.Nonempty segment frontier	StrictConvex	—	strictConvex' Set.Pairwise.imp_on segment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing segment_subset Set.mem_image_of_mem
strictConvex' 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Pairwise Set Set.instSDiff interior Set.instMembership DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap	StrictConvex	—	strictConvex_iff_openSegment_subset openSegment_interior_self_subset_interior openSegment_self_interior_subset_interior HasSubset.Subset.trans Set.instIsTransSubset openSegment_subset_union Set.insert_subset_iff Set.union_subset
subset_interior_image_homothety_of_one_lt 📖	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 Set.instMembership interior Real.instLT Real.instOne	Set.instHasSubset Set.image DFunLike.coe AffineMap CommRing.toRing Real.commRing addGroupIsAddTorsor AffineMap.instFunLike AffineMap.homothety	—	HasSubset.Subset.trans Set.instIsTransSubset subset_closure closure_subset_interior_image_homothety_of_one_lt

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convex 📖	mathematical	IsPreconnected Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Convex Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id	—	Real.convex_iff_isPreconnected

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_eq_openSegment 📖	mathematical	Real instLT instZero	Metric.ball pseudoMetricSpace openSegment semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id instSub instAdd	—	ball_eq_Ioo openSegment_eq_Ioo instIsStrictOrderedRing LT.lt.trans sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_add_of_pos_right
closedBall_eq_segment 📖	mathematical	Real instLE instZero	Metric.closedBall pseudoMetricSpace segment semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id instSub instAdd	—	closedBall_eq_Icc segment_eq_Icc instIsStrictOrderedRing LE.le.trans sub_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_add_of_nonneg_right
convex_iff_isPreconnected 📖	mathematical	—	Convex Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	convex_iff_ordConnected instIsStrictOrderedRing isPreconnected_iff_ordConnected instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_convexHull 📖	mathematical	—	IsClosed DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid	—	IsCompact.isClosed isCompact_convexHull
isCompact_convexHull 📖	mathematical	—	IsCompact DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid	—	IsScalarTower.left convexHull_eq_image Real.instIsStrictOrderedRing IsCompact.image isCompact_stdSimplex LinearMap.continuous_on_pi Finite.of_fintype IsTopologicalAddGroup.toContinuousAdd

(root)

Definitions

Name	Category	Theorems
closedConvexHull 📖	CompOp	10 math math: subset_closedConvexHull, closedConvexHull_min, closedConvexHull_eq_closure_convexHull, closedConvexHull_closure_eq_closedConvexHull, toWeakSpace_closedConvexHull_eq, closure_subset_closedConvexHull, convex_closedConvexHull, isClosed_closedConvexHull, closedConvexHull_isClosed, convexHull_subset_closedConvexHull

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedConvexHull_closure_eq_closedConvexHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull closure	—	subset_antisymm Set.instAntisymmSubset ClosureOperator.idempotent ClosureOperator.monotone closure_subset_closedConvexHull subset_closure
closedConvexHull_eq_closure_convexHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield closure convexHull AddCommGroup.toAddCommMonoid	—	subset_antisymm Set.instAntisymmSubset closedConvexHull_min subset_trans Set.instIsTransSubset subset_convexHull subset_closure Convex.closure convex_convexHull isClosed_closure closure_minimal convexHull_subset_closedConvexHull isClosed_closedConvexHull
closedConvexHull_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra closedConvexHull Convex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsClosed	—	—
closedConvexHull_min 📖	mathematical	Set Set.instHasSubset Convex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull	—	ClosureOperator.closure_min
closure_openSegment 📖	mathematical	—	closure openSegment Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction segment	—	segment_eq_image covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing openSegment_eq_image closure_Ioo zero_ne_one' NeZero.charZero_one IsStrictOrderedRing.toCharZero image_closure_of_isCompact Bornology.IsBounded.isCompact_closure Metric.isBounded_Ioo Continuous.continuousOn Continuous.fun_add Continuous.smul Continuous.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuous_const continuous_id'
closure_subset_closedConvexHull 📖	mathematical	—	Set Set.instHasSubset closure DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull	—	closure_minimal subset_closedConvexHull isClosed_closedConvexHull
convexHull_subset_closedConvexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull AddCommGroup.toAddCommMonoid closedConvexHull	—	convexHull_min subset_closedConvexHull convex_closedConvexHull
convex_closedConvexHull 📖	mathematical	—	Convex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull	—	ClosureOperator.isClosed_closure
convex_closed_sInter 📖	mathematical	Convex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsClosed	Set.sInter	—	starConvex_sInter isClosed_sInter
isClosed_closedConvexHull 📖	mathematical	—	IsClosed DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull	—	ClosureOperator.isClosed_closure
segment_subset_closure_openSegment 📖	mathematical	—	Set Set.instHasSubset segment Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction closure openSegment	—	segment_eq_image covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing openSegment_eq_image closure_Ioo zero_ne_one' NeZero.charZero_one IsStrictOrderedRing.toCharZero image_closure_subset_closure_image Continuous.fun_add Continuous.smul Continuous.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuous_const continuous_id'
subset_closedConvexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull	—	ClosureOperator.le_closure

---

← Back to Index