Topology

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

Statistics

Metric	Count
Definitions closedConvexHull	1
Theorems isClosed_closedInterior, isCompact_closedInterior, 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	53
Total	54

Affine.Simplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_closedInterior 📖	mathematical	—	IsClosed closedInterior DivisionRing.toRing Field.toDivisionRing SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsCompact.isClosed isCompact_closedInterior
isCompact_closedInterior 📖	mathematical	—	IsCompact closedInterior DivisionRing.toRing Field.toDivisionRing SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	AffineEquiv.injective closedInterior_map convexHull_eq_closedInterior IsStrictOrderedRing.toIsOrderedRing Set.Finite.isCompact_convexHull Set.finite_range Finite.of_fintype Homeomorph.isCompact_image Set.image_congr

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 Set.instHasSubset Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing interior_closure_eq_interior_of_nonempty_interior ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring nontrivial_iff_nonempty_interior interior_subset
add_smul_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 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	add_smul_mem_interior' subset_closure
add_smul_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 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction 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	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 interior	—	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 Set.instHasSubset closure Set.image DFunLike.coe AffineMap Real CommRing.toRing Real.commRing addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.homothety interior	—	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 Set.instHasSubset closure interior Set.image DFunLike.coe AffineMap Real CommRing.toRing Real.commRing addGroupIsAddTorsor AddCommGroup.toAddGroup 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	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 AddCommGroup.toAddCommMonoid Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	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 AddCommGroup.toAddCommMonoid Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction interior closure	—	Set.add_subset_add Set.Subset.rfl smul_closure_subset IsOpen.add_closure isOpen_interior subset_interior_add_left SeparatelyContinuousAdd.to_continuousVAdd_op instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	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 AddCommGroup.toAddCommMonoid Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction 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	Set Set.instMembership interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction	—	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 AddCommGroup.toAddCommMonoid Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction 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	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	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 Set.instSDiff Set.instSingletonSet Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 Set.instSDiff Set.instSingletonSet Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 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 Set Set.instInter Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 Set Set.instInter Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 Set.instHasSubset openSegment 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	—	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 Set.instHasSubset openSegment 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	—	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 Set.instHasSubset openSegment 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	—	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 Set.instHasSubset openSegment 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	—	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 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	—	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 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	—	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 Set.instHasSubset interior Set.image DFunLike.coe AffineMap Real CommRing.toRing Real.commRing addGroupIsAddTorsor AddCommGroup.toAddGroup 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 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 Real 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_add_of_pos_right
closedBall_eq_segment 📖	mathematical	Real instLE instZero	Metric.closedBall Real 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	IsScalarTower.left convexHull_eq_image IsCompact.image isCompact_stdSimplex IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing 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	Set Set.instHasSubset 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.comp' continuous_add Continuous.prodMk 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	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 Set.sInter IsClosed	—	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.comp' continuous_add Continuous.prodMk 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