Join

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

Statistics

Metric	Count
Definitions Join, Join, convexJoin	3
Theorems convexHull_union, convexJoin, convexHull_insert, convexHull_union, convexJoin_assoc, convexJoin_assoc_aux, convexJoin_comm, convexJoin_convexJoin_convexJoin_comm, convexJoin_empty_left, convexJoin_empty_right, convexJoin_iUnion_left, convexJoin_iUnion_right, convexJoin_left_comm, convexJoin_mono, convexJoin_mono_left, convexJoin_mono_right, convexJoin_right_comm, convexJoin_segment_singleton, convexJoin_segments, convexJoin_singleton_left, convexJoin_singleton_right, convexJoin_singleton_segment, convexJoin_singletons, convexJoin_subset, convexJoin_subset_convexHull, convexJoin_union_left, convexJoin_union_right, mem_convexJoin, segment_subset_convexJoin, subset_convexJoin_left, subset_convexJoin_right	31
Total	34

CategoryTheory

Definitions

Name	Category	Theorems
Join 📖	CompData	122 math math: Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, Join.inlCompFromSum_hom_app, Join.mapPairId_hom_app, Join.mapWhiskerLeft_app, Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, Join.mapPairEquiv_inverse, Join.mapPairEquiv_unitIso, Join.mapPairEquiv_counitIso, Join.inclRightCompOpEquivInverse_inv_app_op, Join.id_right, Join.mapWhiskerRight_leftUnitor_hom, Join.isoMkFunctor_hom_app, Join.mapWhiskerLeft_whiskerRight, Join.isEquivalenceMapPair, Join.mkFunctor_obj_left, Join.opEquiv_functor_obj_op_right, Join.mapWhiskerLeft_whiskerLeft, Join.inrCompFromSum_hom_app, Join.mkFunctor_edgeTransform, Join.mapPair_obj_right, Join.mapIsoWhiskerLeft_hom, Join.mapPair_map_inclRight, Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, Join.instFinalInclRightOfIsConnected, Join.opEquiv_inverse_map_inclRight_op, Join.mkFunctor_map_inclLeft, Join.mapWhiskerRight_comp, Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, Join.inclRightFaithful, Join.mapWhiskerRight_whiskerRight, Join.mkFunctor_map_inclRight, Join.mapPairComp_hom_app_right, Join.mapWhiskerRight_app, Join.mapWhiskerLeft_whiskerRight_assoc, Join.mapPair_map_inclLeft, Join.isoMkFunctor_inv_app, Join.mapIsoWhiskerRight_inv, Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, Join.fromSum_map_inr, Join.opEquiv_functor_map_op_edge, Join.mapIsoWhiskerRight_hom_app, Join.opEquiv_functor_map_op_inclRight, Join.opEquiv_inverse_obj_right_op, Join.mkFunctorLeft_hom_app, Join.mapWhiskerLeft_associator_hom, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, Join.inclLeft_obj, Join.mapPairComp_inv_app_right, Join.mapPairLeft_inv_app, Join.pseudofunctorRight_mapId_hom_toNatTrans_app, Join.opEquiv_inverse_map_inclLeft_op, Join.homInduction_left, Join.InclLeftCompRightOpOpEquivFunctor_hom_app, Join.mapWhiskerRight_associator_hom, Join.inclRightCompOpEquivInverse_hom_app_op, Join.pseudofunctorRight_mapId_inv_toNatTrans_app, Join.homInduction_right, Join.inclRight_obj, Join.opEquiv_functor_obj_op_left, Join.opEquiv_inverse_obj_left_op, Join.instFaithfulSumFromSum, Join.mapWhisker_exchange, Join.inclLeftCompOpEquivInverse_inv_app_op, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Join.mapPairId_inv_app, Join.mapWhiskerRight_whiskerLeft, Join.inclRightFull, Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, Join.mapWhiskerRight_whiskerLeft_assoc, Join.mkFunctor_map_edge, Join.mapPairComp_hom_app_left, Join.inclLeftCompOpEquivInverse_hom_app_op, Join.mapWhiskerLeft_associator_hom_assoc, Join.mapWhiskerLeft_rightUnitor_hom, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, Join.mapWhiskerRight_id, Join.mapWhiskerRight_rightUnitor_hom, Join.opEquiv_inverse_map_edge_op, Join.mapPairComp_inv_app_left, Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, Join.InclLeftCompRightOpOpEquivFunctor_inv_app, Join.mapIsoWhiskerRight_hom, Join.instInitialInclLeftOfIsConnected, Join.mapPair_obj_left, Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, Join.InclRightCompRightOpOpEquivFunctor_inv_app, Join.mkFunctorRight_inv_app, Join.mapWhiskerLeft_whiskerLeft_assoc, Join.mapWhiskerLeft_id, Join.mapWhiskerRight_whiskerRight_assoc, Join.mapWhiskerLeft_leftUnitor_hom, Join.fromSum_obj, Join.inrCompFromSum_inv_app, Join.mkFunctorLeft_inv_app, Join.mapPairLeft_hom_app, Join.mapIsoWhiskerLeft_inv_app, Join.mkFunctor_obj_right, Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Join.mapPairRight_hom_app, Join.opEquiv_functor_map_op_inclLeft, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, Join.id_left, Join.mapIsoWhiskerLeft_hom_app, Join.eq_mkNatTrans, Join.mapPairEquiv_functor, Join.instEssSurjSumFromSum, Join.fromSum_map_inl, Join.mapIsoWhiskerLeft_inv, Join.inclLeftFull, Join.mapWhiskerLeft_comp, Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, Join.InclRightCompRightOpOpEquivFunctor_hom_app, Join.mapPairRight_inv_app, Join.mkFunctorRight_hom_app, Join.inlCompFromSum_inv_app, Join.inclLeftFaithful, Join.edgeTransform_app, Join.mapIsoWhiskerRight_inv_app, Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull_union 📖	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	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instUnion convexJoin	—	HasSubset.Subset.antisymm Set.instAntisymmSubset convexHull_min Set.union_subset subset_convexJoin_left IsStrictOrderedRing.toIsOrderedRing subset_convexJoin_right convexJoin convexJoin_subset_convexHull
convexJoin 📖	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	convexJoin	—	exists_mem_add_smul_eq mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing add_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₃ Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass

Relation

Definitions

Name	Category	Theorems
Join 📖	MathDef	15 math math: FreeGroup.Red.church_rosser, FreeGroup.join_red_of_step, church_rosser, FreeAddGroup.join_red_of_step, FreeAddGroup.Red.church_rosser, FreeGroup.equivalence_join_red, reflexive_join, FreeAddGroup.Red.exact, FreeGroup.Red.exact, symmetric_join, FreeAddGroup.equivalence_join_red, join_of_single, equivalence_join_reflTransGen, FreeGroup.eqvGen_step_iff_join_red, FreeAddGroup.eqvGen_step_iff_join_red

(root)

Definitions

Name	Category	Theorems
convexJoin 📖	CompOp	31 math math: convexHull_insert, convexJoin_singletons, convexJoin_subset, convexJoin_singleton_left, convexJoin_segments, convexJoin_union_right, convexJoin_iUnion_right, convexJoin_mono, Convex.convexHull_union, convexJoin_mono_right, segment_subset_convexJoin, convexJoin_segment_singleton, convexJoin_singleton_segment, convexJoin_empty_left, convexJoin_iUnion_left, convexJoin_assoc, convexJoin_mono_left, convexJoin_subset_convexHull, convexJoin_convexJoin_convexJoin_comm, convexJoin_empty_right, convexJoin_union_left, subset_convexJoin_left, subset_convexJoin_right, convexJoin_left_comm, convexJoin_assoc_aux, convexJoin_right_comm, convexHull_union, convexJoin_comm, Convex.convexJoin, mem_convexJoin, convexJoin_singleton_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull_insert 📖	mathematical	Set.Nonempty	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 Set.instInsert convexJoin Set.instSingletonSet	—	Set.insert_eq convexHull_union Set.singleton_nonempty convexHull_singleton
convexHull_union 📖	mathematical	Set.Nonempty	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 Set.instUnion convexJoin	—	convexHull_convexHull_union_left convexHull_convexHull_union_right Convex.convexHull_union convex_convexHull Set.Nonempty.convexHull
convexJoin_assoc 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	HasSubset.Subset.antisymm Set.instAntisymmSubset convexJoin_assoc_aux convexJoin_comm
convexJoin_assoc_aux 📖	mathematical	—	Set Set.instHasSubset convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	LE.le.eq_or_lt left_mem_segment IsStrictOrderedRing.toZeroLEOneClass Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.smul_eq_const Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₂ add_zero Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eq_cons_const eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid le_of_lt div_pos Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.Module.NF.eq_cons_cons Mathlib.Tactic.FieldSimp.NF.cons_ne_zero
convexJoin_comm 📖	mathematical	—	convexJoin	—	Set.iUnion₂_comm Set.iUnion_congr_Prop segment_symm
convexJoin_convexJoin_convexJoin_comm 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	convexJoin_right_comm
convexJoin_empty_left 📖	mathematical	—	convexJoin Set Set.instEmptyCollection	—	Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty
convexJoin_empty_right 📖	mathematical	—	convexJoin Set Set.instEmptyCollection	—	Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty
convexJoin_iUnion_left 📖	mathematical	—	convexJoin Set.iUnion	—	Set.iUnion_congr_Prop Set.iUnion_exists Set.iUnion_comm
convexJoin_iUnion_right 📖	mathematical	—	convexJoin Set.iUnion	—	convexJoin_comm convexJoin_iUnion_left
convexJoin_left_comm 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	convexJoin_comm
convexJoin_mono 📖	mathematical	Set Set.instHasSubset	convexJoin	—	Set.biUnion_mono Set.biUnion_subset_biUnion_left
convexJoin_mono_left 📖	mathematical	Set Set.instHasSubset	convexJoin	—	convexJoin_mono Set.Subset.rfl
convexJoin_mono_right 📖	mathematical	Set Set.instHasSubset	convexJoin	—	convexJoin_mono Set.Subset.rfl
convexJoin_right_comm 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	—	convexJoin_assoc convexJoin_comm
convexJoin_segment_singleton 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid 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 Set Set.instSingletonSet DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instInsert	—	Set.pair_eq_singleton convexJoin_segments segment_same IsStrictOrderedRing.toZeroLEOneClass
convexJoin_segments 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid 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 DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instInsert Set.instSingletonSet	—	IsStrictOrderedRing.toIsOrderedRing convexHull_insert Set.insert_nonempty Set.singleton_nonempty convexJoin_assoc convexHull_singleton
convexJoin_singleton_left 📖	mathematical	—	convexJoin Set Set.instSingletonSet Set.iUnion Set.instMembership segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
convexJoin_singleton_right 📖	mathematical	—	convexJoin Set Set.instSingletonSet Set.iUnion Set.instMembership segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
convexJoin_singleton_segment 📖	mathematical	—	convexJoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid Set Set.instSingletonSet 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 DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instInsert	—	segment_same IsStrictOrderedRing.toZeroLEOneClass convexJoin_segments Set.insert_idem
convexJoin_singletons 📖	mathematical	—	convexJoin Set Set.instSingletonSet segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	convexJoin_singleton_right Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
convexJoin_subset 📖	mathematical	Set Set.instHasSubset Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	convexJoin	—	Set.iUnion₂_subset Convex.segment_subset
convexJoin_subset_convexHull 📖	mathematical	—	Set Set.instHasSubset convexJoin DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instUnion	—	convexJoin_subset HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left subset_convexHull Set.subset_union_right convex_convexHull
convexJoin_union_left 📖	mathematical	—	convexJoin Set Set.instUnion	—	Set.iUnion_congr_Prop Set.iUnion_or Set.iUnion_union_distrib
convexJoin_union_right 📖	mathematical	—	convexJoin Set Set.instUnion	—	convexJoin_comm convexJoin_union_left
mem_convexJoin 📖	mathematical	—	Set Set.instMembership convexJoin segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
segment_subset_convexJoin 📖	mathematical	Set Set.instMembership	Set.instHasSubset segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction convexJoin	—	Set.subset_iUnion₂_of_subset Set.subset_iUnion₂
subset_convexJoin_left 📖	mathematical	Set.Nonempty	Set Set.instHasSubset convexJoin	—	segment_subset_convexJoin left_mem_segment IsOrderedRing.toZeroLEOneClass
subset_convexJoin_right 📖	mathematical	Set.Nonempty	Set Set.instHasSubset convexJoin	—	subset_convexJoin_left convexJoin_comm

---

← Back to Index