Segment

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

Statistics

Metric	Count
Definitions «term[_-[_]_]», openSegment, segment	3
Theorems combo_le_max, mem_Icc, mem_Ico, mem_Ioc, mem_Ioo, min_le_combo, Icc_subset_segment, Ioo_subset_openSegment, Icc_subset_segment, segment_eq_Icc, segment_eq_uIcc, image_update_openSegment, image_update_segment, openSegment_subset, segment_subset, image_mk_openSegment_left, image_mk_openSegment_right, image_mk_segment_left, image_mk_segment_right, openSegment_subset, segment_subset, image_openSegment, image_segment, insert_endpoints_openSegment, left_mem_openSegment_iff, left_mem_segment, lineMap_mem_openSegment, mem_openSegment_iff_div, mem_openSegment_of_ne_left_right, mem_openSegment_translate, mem_segment_add_sub, mem_segment_iff_div, mem_segment_iff_sameRay, mem_segment_sub_add, mem_segment_translate, midpoint_mem_segment, openSegment_eq_Ioo, openSegment_eq_Ioo', openSegment_eq_image, openSegment_eq_image', openSegment_eq_image_lineMap, openSegment_eq_image₂, openSegment_same, openSegment_subset_Ioo, openSegment_subset_iff, openSegment_subset_iff_segment_subset, openSegment_subset_segment, openSegment_subset_union, openSegment_symm, openSegment_translate_image, openSegment_translate_preimage, right_mem_openSegment_iff, right_mem_segment, sameRay_of_mem_segment, segment_eq_Icc, segment_eq_Icc', segment_eq_image, segment_eq_image', segment_eq_image_lineMap, segment_eq_image₂, segment_eq_uIcc, segment_inter_eq_endpoint_of_linearIndependent_of_ne, segment_inter_eq_endpoint_of_linearIndependent_sub, segment_inter_subset_endpoint_of_linearIndependent_sub, segment_same, segment_subset_Icc, segment_subset_iff, segment_subset_uIcc, segment_symm, segment_translate_image, segment_translate_preimage, vadd_openSegment, vadd_segment	73
Total	76

Convex

Definitions

Name	Category	Theorems
«term[_-[_]_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
combo_le_max 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup	—	segment_subset_uIcc
mem_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Set.Icc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Distrib.toMul	—	segment_eq_Icc
mem_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Set.Ico 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 Distrib.toMul	—	mem_Icc LT.lt.le Set.Ico_subset_Icc_self LE.le.eq_or_lt LT.lt.ne zero_add MulZeroClass.zero_mul one_mul add_zero Set.left_mem_Ico Set.Ioo_subset_Ico_self mem_Ioo
mem_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Set.Ioc Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Distrib.toMul	—	mem_Icc LT.lt.le Set.Ioc_subset_Icc_self LE.le.eq_or_lt LT.lt.ne add_zero MulZeroClass.zero_mul one_mul zero_add Set.right_mem_Ioc Set.Ioo_subset_Ioc_self mem_Ioo
mem_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Set.Ioo MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Distrib.toMul	—	openSegment_eq_Ioo
min_le_combo 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	segment_subset_uIcc

Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_subset_segment 📖	mathematical	—	Set Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.instHasSubset Set.Icc Subtype.preorder segment semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Subtype.partialOrder addCommMonoid Algebra.toSMul commSemiring Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Icc_subset_segment Subtype.coe_le_coe zero_le canonicallyOrderedAdd
segment_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	segment semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Subtype.partialOrder addCommMonoid Algebra.toSMul commSemiring Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc Subtype.preorder	—	subset_antisymm IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Set.instAntisymmSubset segment_subset_Icc isOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule isStrictOrderedRing Icc_subset_segment
segment_eq_uIcc 📖	mathematical	—	segment Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Subtype.partialOrder addCommMonoid Algebra.toSMul commSemiring Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set.uIcc distribLattice	—	IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono le_total segment_eq_Icc Set.uIcc_of_le segment_symm Set.uIcc_of_ge

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_update_openSegment 📖	mathematical	—	Set.image Function.update openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction addCommMonoid instSMul	—	openSegment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
image_update_segment 📖	mathematical	—	Set.image Function.update segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction addCommMonoid instSMul	—	segment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
openSegment_subset 📖	mathematical	—	Set Set.instHasSubset openSegment addCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.pi	—	—
segment_subset 📖	mathematical	—	Set Set.instHasSubset segment addCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.pi	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_mk_openSegment_left 📖	mathematical	—	Set.image openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid instSMul	—	openSegment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
image_mk_openSegment_right 📖	mathematical	—	Set.image openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid instSMul	—	openSegment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
image_mk_segment_left 📖	mathematical	—	Set.image segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid instSMul	—	segment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
image_mk_segment_right 📖	mathematical	—	Set.image segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid instSMul	—	segment_eq_image₂ Set.image_image Set.EqOn.image_eq Convex.combo_self
openSegment_subset 📖	mathematical	—	Set Set.instHasSubset openSegment instAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SProd.sprod Set.instSProd	—	—
segment_subset 📖	mathematical	—	Set Set.instHasSubset segment instAddCommMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SProd.sprod Set.instSProd	—	—

(root)

Definitions

Name	Category	Theorems
openSegment 📖	CompOp	53 math math: Pi.image_update_openSegment, openSegment_subset_iff, Prod.image_mk_openSegment_left, MeasureTheory.average_mem_openSegment_compl_self, openSegment_eq_Ioo, Convex.openSegment_self_interior_subset_interior, openSegment_translate_image, convex_iff_openSegment_subset, mem_openSegment_translate, openSegment_eq_Ioo', openSegment_eq_image', image_openSegment, ConvexOn.openSegment_subset_strict_epigraph, openSegment_subset_ball_of_ne, Convex.openSegment_interior_self_subset_interior, mem_openSegment_of_ne_left_right, lineMap_mem_openSegment, Real.ball_eq_openSegment, convex_openSegment, StarConvex.openSegment_subset, strictConvex_iff_openSegment_subset, StrictConvex.openSegment_subset, starConvex_iff_openSegment_subset, closure_openSegment, openSegment_eq_image, openSegment_subset_segment, right_mem_openSegment_iff, Convex.openSegment_subset, insert_endpoints_openSegment, Prod.openSegment_subset, Prod.image_mk_openSegment_right, openSegment_eq_image_lineMap, Ioo_subset_openSegment, ConcaveOn.openSegment_subset_strict_hypograph, openSegment_symm, vadd_openSegment, Pi.openSegment_subset, MeasureTheory.laverage_mem_openSegment_compl_self, openSegment_eq_image₂, openSegment_translate_preimage, Convex.openSegment_closure_interior_subset_interior, mem_openSegment_of_gauge_lt_one, openSegment_same, openSegment_subset_Ioo, mem_openSegment_iff_div, MeasureTheory.laverage_union_mem_openSegment, left_mem_openSegment_iff, segment_subset_closure_openSegment, MeasureTheory.average_union_mem_openSegment, Convex.openSegment_interior_closure_subset_interior, openSegment_subset_union, openSegment.lift, openSegment_subset_iff_segment_subset
segment 📖	CompOp	76 math math: segment_subset_closedBall_right, MeasureTheory.hausdorffMeasure_segment, convexJoin_singletons, segment_inter_subset_endpoint_of_linearIndependent_sub, segment_translate_preimage, segment_eq_image₂, convexJoin_singleton_left, stdSimplex_fin_two, NNReal.segment_eq_uIcc, convexJoin_segments, left_mem_segment, Prod.segment_subset, segment_eq_uIcc, segment_subset_convexHull, Nonneg.segment_eq_uIcc, segment_single_subset_stdSimplex, segment_subset_convexJoin, convexJoin_segment_singleton, convexJoin_singleton_segment, Prod.image_mk_segment_left, segment_symm, segment_eq_Icc', starConvex_iff_segment_subset, segment_eq_image, mem_segment_iff_sameRay, closure_openSegment, segment_eq_Icc, segment_inter_eq_endpoint_of_linearIndependent_of_ne, openSegment_subset_segment, convexHull_pair, insert_endpoints_openSegment, vadd_segment, Path.range_segment, segment_subset_Icc, Prod.image_mk_segment_right, Real.closedBall_eq_segment, vectorSpan_segment, segment_same, segment_subset_closedBall_left, MeasureTheory.average_union_mem_segment, segment_eq_image', image_segment, StarConvex.segment_subset, affineSegment_eq_segment, MeasureTheory.laverage_union_mem_segment, NNReal.segment_eq_Icc, segment_translate_image, parallelepiped_eq_sum_segment, mem_segment_iff_wbtw, right_mem_segment, mem_segment_iff_div, convex_iff_segment_subset, segment_eq_image_lineMap, midpoint_mem_segment, Real.dimH_segment, segment_subset_uIcc, segment_subset_iff, segment.lift, mem_segment_add_sub, Pi.image_update_segment, Nonneg.Icc_subset_segment, Pi.segment_subset, segment_subset_closure_openSegment, mem_segment_translate, mem_convexJoin, convexJoin_singleton_right, Convex.segment_subset, Wbtw.mem_segment, segment_inter_eq_endpoint_of_linearIndependent_sub, domain_mvt, openSegment_subset_iff_segment_subset, mem_segment_sub_add, Icc_subset_segment, convex_segment, Nonneg.segment_eq_Icc, NNReal.Icc_subset_segment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_subset_segment 📖	mathematical	—	Set Set.instHasSubset Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder segment DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	LE.le.eq_or_lt LE.le.trans segment_same IsStrictOrderedRing.toZeroLEOneClass LE.le.antisymm div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing LT.lt.le sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd add_div sub_add_sub_cancel div_self LT.lt.ne' smul_eq_mul mul_div_right_comm div_eq_iff add_comm sub_mul mul_comm mul_sub
Ioo_subset_openSegment 📖	mathematical	—	Set Set.instHasSubset Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder openSegment DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	mem_openSegment_of_ne_left_right IsStrictOrderedRing.toZeroLEOneClass LT.lt.ne LT.lt.ne' Icc_subset_segment Set.Ioo_subset_Icc_self
image_openSegment 📖	mathematical	—	Set.image DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike openSegment Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.ext openSegment_eq_image_lineMap AffineMap.apply_lineMap
image_segment 📖	mathematical	—	Set.image DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike segment Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.ext segment_eq_image_lineMap AffineMap.apply_lineMap
insert_endpoints_openSegment 📖	mathematical	—	Set Set.instInsert openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction segment	—	Set.instReflSubset Set.instAntisymmSubset add_zero one_smul zero_smul zero_add LE.le.eq_or_lt
left_mem_openSegment_iff 📖	mathematical	—	Set Set.instMembership 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	—	smul_right_injective IsDomain.toIsCancelMulZero IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE LT.lt.ne' AddLeftCancelSemigroup.toIsLeftCancelAdd add_smul one_smul openSegment_same covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Set.mem_singleton
left_mem_segment 📖	mathematical	—	Set Set.instMembership segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero MulActionWithZero.toSMulWithZero	—	zero_le_one le_refl add_zero zero_smul one_smul
lineMap_mem_openSegment 📖	mathematical	Set Set.instMembership Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	openSegment Ring.toSemiring 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 AffineMap Ring.toAddCommGroup Semiring.toModule addGroupIsAddTorsor AddGroupWithOne.toAddGroup AffineMap.instFunLike AffineMap.lineMap	—	Set.mem_image_of_mem openSegment_eq_image_lineMap
mem_openSegment_iff_div 📖	mathematical	—	Set Set.instMembership openSegment DivisionSemiring.toSemiring Semifield.toDivisionSemiring 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 Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	div_one add_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono add_div div_self LT.lt.ne'
mem_openSegment_of_ne_left_right 📖	mathematical	Set Set.instMembership segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	openSegment	—	insert_endpoints_openSegment
mem_openSegment_translate 📖	mathematical	—	Set Set.instMembership openSegment Ring.toSemiring 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	vaddCommClass_self
mem_segment_add_sub 📖	mathematical	—	Set Set.instMembership 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub	—	Nat.instAtLeastTwoHAddOfNat midpoint_add_sub midpoint_mem_segment
mem_segment_iff_div 📖	mathematical	—	Set Set.instMembership segment DivisionSemiring.toSemiring Semifield.toDivisionSemiring 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 Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero div_one Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono add_div div_self LT.lt.ne'
mem_segment_iff_sameRay 📖	mathematical	—	Set Set.instMembership segment 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 SameRay Semifield.toCommSemiring SubNegMonoid.toSub	—	sameRay_of_mem_segment SameRay.exists_eq_smul_add mem_segment_translate covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing neg_add_cancel add_comm sub_eq_neg_add neg_sub sub_add_sub_cancel smul_neg SMulCommClass.smul_comm smulCommClass_self
mem_segment_sub_add 📖	mathematical	—	Set Set.instMembership 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 SubNegMonoid.toSub AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Nat.instAtLeastTwoHAddOfNat midpoint_sub_add midpoint_mem_segment
mem_segment_translate 📖	mathematical	—	Set Set.instMembership segment Ring.toSemiring 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	vaddCommClass_self
midpoint_mem_segment 📖	mathematical	—	Set Set.instMembership 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 midpoint addGroupIsAddTorsor	—	Nat.instAtLeastTwoHAddOfNat segment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing invOf_nonneg zero_le_two IsStrictOrderedRing.toZeroLEOneClass invOf_le_one one_le_two
openSegment_eq_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	openSegment DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioo	—	HasSubset.Subset.antisymm Set.instAntisymmSubset openSegment_subset_Ioo IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Ioo_subset_openSegment
openSegment_eq_Ioo' 📖	mathematical	—	openSegment 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.Ioo PartialOrder.toPreorder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Ne.lt_or_gt openSegment_eq_Ioo max_eq_right LT.lt.le min_eq_left openSegment_symm max_eq_left min_eq_right
openSegment_eq_image 📖	mathematical	—	openSegment Ring.toSemiring 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.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Set.ext lt_add_of_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd add_sub_cancel_right sub_pos sub_add_cancel
openSegment_eq_image' 📖	mathematical	—	openSegment Ring.toSemiring 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.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Set.image_congr smul_sub sub_smul one_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero openSegment_eq_image
openSegment_eq_image_lineMap 📖	mathematical	—	openSegment Ring.toSemiring 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.image DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Set.image_congr AffineMap.lineMap_apply_module openSegment_eq_image
openSegment_eq_image₂ 📖	mathematical	—	openSegment Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup setOf Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
openSegment_same 📖	mathematical	—	openSegment Ring.toSemiring 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.instSingletonSet	—	Set.ext one_smul DenselyOrdered.dense zero_lt_one NeZero.one sub_pos_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd add_sub_cancel add_smul
openSegment_subset_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Set Set.instHasSubset openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ioo	—	Convex.combo_self add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid smul_lt_smul_of_pos_left add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add
openSegment_subset_iff 📖	mathematical	—	Set Set.instHasSubset openSegment Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
openSegment_subset_iff_segment_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset openSegment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction segment	—	—
openSegment_subset_segment 📖	mathematical	—	Set Set.instHasSubset openSegment segment	—	LT.lt.le
openSegment_subset_union 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap	Set.instHasSubset openSegment 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 DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.instInsert Set.instUnion	—	openSegment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_trichotomy LT.lt.trans div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono div_lt_one div_mul_cancel₀ LT.lt.ne' sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Set.image_congr AffineMap.lineMap_apply_one_sub sub_lt_sub_right sub_mul one_mul sub_sub_sub_cancel_right
openSegment_symm 📖	mathematical	—	openSegment	—	Set.ext add_comm
openSegment_translate_image 📖	mathematical	—	Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid openSegment Ring.toSemiring 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.image_preimage_eq openSegment_translate_preimage add_left_surjective
openSegment_translate_preimage 📖	mathematical	—	Set.preimage AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid openSegment Ring.toSemiring 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.ext mem_openSegment_translate
right_mem_openSegment_iff 📖	mathematical	—	Set Set.instMembership 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	—	openSegment_symm left_mem_openSegment_iff
right_mem_segment 📖	mathematical	—	Set Set.instMembership segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero MulActionWithZero.toSMulWithZero	—	left_mem_segment segment_symm
sameRay_of_mem_segment 📖	mathematical	Set Set.instMembership segment CommSemiring.toSemiring CommRing.toCommSemiring 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	SameRay SubNegMonoid.toSub	—	segment_eq_image' covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing SameRay.congr_simp add_sub_cancel_left sub_smul one_smul SameRay.nonneg_smul_right PosSMulMono.toSMulPosMono IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule IsScalarTower.left SameRay.sameRay_nonneg_smul_left sub_nonneg
segment_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	segment DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc	—	HasSubset.Subset.antisymm Set.instAntisymmSubset segment_subset_Icc IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Icc_subset_segment
segment_eq_Icc' 📖	mathematical	—	segment 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.Icc PartialOrder.toPreorder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total segment_eq_Icc max_eq_right min_eq_left segment_symm max_eq_left min_eq_right
segment_eq_image 📖	mathematical	—	segment Ring.toSemiring 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.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Set.ext le_add_of_nonneg_left add_sub_cancel_right sub_nonneg sub_add_cancel
segment_eq_image' 📖	mathematical	—	segment Ring.toSemiring 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.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Set.image_congr smul_sub sub_smul one_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero segment_eq_image
segment_eq_image_lineMap 📖	mathematical	—	segment Ring.toSemiring 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.image DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Set.image_congr AffineMap.lineMap_apply_module segment_eq_image
segment_eq_image₂ 📖	mathematical	—	segment Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup setOf Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
segment_eq_uIcc 📖	mathematical	—	segment 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.uIcc	—	segment_eq_Icc'
segment_inter_eq_endpoint_of_linearIndependent_of_ne 📖	mathematical	LinearIndependent Matrix.vecCons Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set Set.instInter segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Set.instSingletonSet	—	segment_inter_eq_endpoint_of_linearIndependent_sub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toIsStrictOrderedRing IsDomain.to_noZeroDivisors IsDomain.toNontrivial add_sub_add_left_eq_sub LinearIndependent.pair_add_smul_add_smul_iff smulCommClass_self IsScalarTower.left instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors NoZeroDivisors.toNoZeroSMulDivisors neg_mul one_mul mul_neg mul_one neg_smul one_smul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.termg_eq add_zero one_zsmul Mathlib.Tactic.Abel.const_add_termg
segment_inter_eq_endpoint_of_linearIndependent_sub 📖	mathematical	LinearIndependent Matrix.vecCons SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Matrix.vecEmpty Ring.toSemiring AddCommGroup.toAddCommMonoid	Set Set.instInter segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.instSingletonSet	—	HasSubset.Subset.antisymm Set.instAntisymmSubset segment_inter_subset_endpoint_of_linearIndependent_sub
segment_inter_subset_endpoint_of_linearIndependent_sub 📖	mathematical	LinearIndependent Matrix.vecCons SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Matrix.vecEmpty Ring.toSemiring AddCommGroup.toAddCommMonoid	Set Set.instHasSubset Set.instInter segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.instSingletonSet	—	Set.mem_image segment_eq_image Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_termg sub_smul one_smul sub_add_add_cancel smul_add LinearIndependent.eq_zero_of_pair' AddLeftCancelSemigroup.toIsLeftCancelAdd sub_zero zero_smul add_zero
segment_same 📖	mathematical	—	segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instSingletonSet	—	Set.ext add_smul one_smul left_mem_segment Set.mem_singleton_iff
segment_subset_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Set Set.instHasSubset segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Icc	—	Convex.combo_self add_le_add_right IsOrderedAddMonoid.toAddLeftMono smul_le_smul_of_nonneg_left add_le_add_left covariant_swap_add_of_covariant_add
segment_subset_iff 📖	mathematical	—	Set Set.instHasSubset segment Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
segment_subset_uIcc 📖	mathematical	—	Set Set.instHasSubset segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total Set.uIcc_of_le segment_subset_Icc Set.uIcc_of_ge segment_symm
segment_symm 📖	mathematical	—	segment	—	Set.ext add_comm
segment_translate_image 📖	mathematical	—	Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid segment Ring.toSemiring 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.image_preimage_eq segment_translate_preimage add_left_surjective
segment_translate_preimage 📖	mathematical	—	Set.preimage AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid segment Ring.toSemiring 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.ext mem_segment_translate
vadd_openSegment 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction openSegment Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	image_openSegment VAddCommClass.vadd_comm
vadd_segment 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction segment Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	image_segment VAddCommClass.vadd_comm

---

← Back to Index