Hull

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

Statistics

Metric	Count
Definitions convexHull	1
Theorems image_convexHull, convexHull_eq, convexHull_subset_iff, convex_remove_iff_notMem_convexHull_remove, image_convexHull, image_convexHull, convexHull, affineSpan_convexHull, convexHull_add_subset, convexHull_convexHull_union_left, convexHull_convexHull_union_right, convexHull_empty, convexHull_eq_empty, convexHull_eq_iInter, convexHull_eq_self, convexHull_eq_singleton, convexHull_eq_zero, convexHull_isClosed, convexHull_min, convexHull_mono, convexHull_neg, convexHull_nonempty_iff, convexHull_pair, convexHull_singleton, convexHull_smul, convexHull_subset_affineSpan, convexHull_univ, convexHull_vadd, convexHull_zero, convex_convexHull, mem_convexHull_iff, segment_subset_convexHull, subset_convexHull	33
Total	34

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_convexHull 📖	mathematical	—	Set.image DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Set.Subset.antisymm Set.image_subset_iff convexHull_min subset_convexHull Convex.affine_preimage convex_convexHull Set.image_mono Convex.affine_image

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull_eq 📖	mathematical	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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	—	convexHull_eq_self
convexHull_subset_iff 📖	mathematical	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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 convexHull	—	ClosureOperator.IsClosed.closure_le_iff
convex_remove_iff_notMem_convexHull_remove 📖	mathematical	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instSDiff Set.instSingletonSet Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	convexHull_eq Set.mem_singleton Set.Subset.antisymm subset_convexHull convexHull_min Set.diff_subset convex_convexHull

IsLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_convexHull 📖	mathematical	IsLinearMap	Set.image DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	Set.Subset.antisymm Set.image_subset_iff convexHull_min subset_convexHull Convex.is_linear_preimage convex_convexHull Set.image_mono Convex.is_linear_image

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_convexHull 📖	mathematical	—	Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	IsLinearMap.image_convexHull isLinear

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull 📖	mathematical	Set.Nonempty	Set.Nonempty DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	convexHull_nonempty_iff

(root)

Definitions

Name	Category	Theorems
convexHull 📖	CompOp	125 math math: convexIndependent_set_iff_inter_convexHull_subset, IsLinearMap.image_convexHull, convexHull_insert, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, rank_le_card_isVisible, convexHull_multiset_sum, Geometry.SimplicialComplex.convexHull_subset_space, Geometry.SimplicialComplex.mem_space_iff, Convex.convex_remove_iff_notMem_convexHull_remove, convexHull_eq_iInter, Complex.convexHull_reProdIm, IsVisible.mem_convexHull_isVisible, convexJoin_segments, convexHull_union_neg_eq_absConvexHull, interior_convexHull_nonempty_iff_affineSpan_eq_top, mem_convexHull_pi, Geometry.SimplicialComplex.convexHull_inter_convexHull, AffineBasis.convexHull_eq_nonneg_coord, segment_subset_convexHull, convexHull_toCone_eq_sInf, Balanced.convexHull, balancedHull_subset_convexHull_union_neg, Convex.convexHull_union, closedConvexHull_eq_closure_convexHull, Finset.mem_convexHull', subset_convexHull, Convex.convexHull_subset_iff, AffineBasis.interior_convexHull, Geometry.SimplicialComplex.inter_subset_convexHull, convexJoin_segment_singleton, convexJoin_singleton_segment, convexHull_diam, Finset.centerMass_id_mem_convexHull, Set.Finite.isCompact_convexHull, Finset.centerMass_id_mem_convexHull_of_nonpos, convexHull_add, affineSpan_convexHull, convexHull_basis_eq_stdSimplex, Convex.radon_partition, ConvexOn.bddAbove_convexHull, ConvexIndependent.mem_convexHull_iff, not_disjoint_segment_convexHull_triple, convexHull_vadd, exists_mem_interior_convexHull_affineBasis, Caratheodory.mem_minCardFinsetOfMemConvexHull, Convex.mem_extremePoints_iff_mem_diff_convexHull_diff, mk_mem_convexHull_prod, convexHull_add_subset, Polynomial.rootSet_derivative_subset_convexHull_rootSet, closure_convexHull_extremePoints, Set.Finite.isClosed_convexHull, convexHull_empty, Finset.centerMass_mem_convexHull, convexHull_pair, convexJoin_subset_convexHull, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, convexHull_eq_empty, convexHull_singleton, convex_convexHull, convexHull_sum, isBounded_convexHull, Finset.mem_convexHull, convexHull_neg, convexIndependent_set_iff_notMem_convexHull_diff, convexHull_sphere_eq_closedBall, Convex.exists_subset_interior_convexHull_finset_of_isCompact, convexHull_mono, convexHullAddMonoidHom_apply, Finset.convexHull_eq, totallyBounded_convexHull, convexHull_eq_singleton, convexHull_eq_zero, convexHull_pi, Caratheodory.mem_convexHull_erase, doublyStochastic_eq_convexHull_permMatrix, Finset.centroid_mem_convexHull, LinearMap.image_convexHull, convexHull_univ, convexHull_ediam, AffineIndependent.convexHull_inter', convexHull_zero, convexHull_eq_union_convexHull_finite_subsets, affineCombination_mem_convexHull, mem_convexHull_iff_exists_fintype, convexHull_toCone_isLeast, extremePoints_convexHull_subset, Geometry.SimplicialComplex.face_subset_face_iff, Convex.convexHull_eq, convexHull_convexHull_union_right, IsClosed.convexHull_subset_affineSpan_isVisible, ConvexOn.le_sup_of_mem_convexHull, convexHull_convexHull_union_left, convexHull_min, convexHull_isClosed, convexHull_prod, convexHull_eq_union, convexHull_eq, convexHull_smul, Set.Nonempty.convexHull, absConvexHull_eq_convexHull_balancedHull, Set.Finite.convexHull_eq_image, mem_convexHull_of_exists_fintype, IsVisible.of_convexHull_of_pos, convexHull_rangle_single_eq_stdSimplex, AffineBasis.centroid_mem_interior_convexHull, AffineMap.image_convexHull, convexHull_union, convexHull_sub, ConcaveOn.bddBelow_convexHull, convexHull_list_sum, convexHull_nonempty_iff, mem_convexHull_iff, parallelepiped_eq_convexHull, ConvexOn.inf_le_of_mem_convexHull, AffineIndependent.convexHull_inter, Set.Finite.convexHull_eq, Affine.Simplex.convexHull_eq_closedInterior, convexHull_subset_affineSpan, convexHull_eq_self, balancedHull_convexHull_subseteq_absConvexHull, convexHull_range_eq_exists_affineCombination, convexIndependent_iff_notMem_convexHull_diff, Complex.rectangle_eq_convexHull, convexHull_subset_closedConvexHull, Finset.centerMass_mem_convexHull_of_nonpos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_convexHull 📖	mathematical	—	affineSpan addGroupIsAddTorsor AddCommGroup.toAddGroup DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Ring.toSemiring AddCommGroup.toAddCommMonoid	—	le_antisymm affineSpan_le convexHull_subset_affineSpan affineSpan_mono subset_convexHull
convexHull_add_subset 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	convexHull_min Set.add_subset_add subset_convexHull Convex.add convex_convexHull
convexHull_convexHull_union_left 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instUnion	—	ClosureOperator.closure_sup_closure_left
convexHull_convexHull_union_right 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instUnion	—	ClosureOperator.closure_sup_closure_right
convexHull_empty 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instEmptyCollection	—	Convex.convexHull_eq convex_empty
convexHull_eq_empty 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instEmptyCollection	—	Set.subset_empty_iff subset_convexHull convexHull_empty
convexHull_eq_iInter 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.iInter Set.instHasSubset Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.iInter_subtype Set.iInter_congr_Prop Set.iInter_and
convexHull_eq_self 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ClosureOperator.isClosed_iff
convexHull_eq_singleton 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instSingletonSet	—	Set.Nonempty.subset_singleton_iff convexHull_empty subset_convexHull convexHull_singleton
convexHull_eq_zero 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	convexHull_eq_singleton
convexHull_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra convexHull Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
convexHull_min 📖	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	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	ClosureOperator.closure_min
convexHull_mono 📖	mathematical	Set Set.instHasSubset	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	ClosureOperator.monotone
convexHull_neg 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Ring.toSemiring AddCommGroup.toAddCommMonoid Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AffineMap.image_convexHull
convexHull_nonempty_iff 📖	mathematical	—	Set.Nonempty DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	Set.nonempty_iff_ne_empty convexHull_eq_empty
convexHull_pair 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instInsert Set.instSingletonSet segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	HasSubset.Subset.antisymm Set.instAntisymmSubset convexHull_min Set.insert_subset_iff Set.singleton_subset_iff left_mem_segment IsOrderedRing.toZeroLEOneClass right_mem_segment convex_segment segment_subset_convexHull Set.mem_insert Set.subset_insert Set.mem_singleton
convexHull_singleton 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.instSingletonSet	—	Convex.convexHull_eq convex_singleton
convexHull_smul 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull CommSemiring.toSemiring Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smulCommClass_self LinearMap.image_convexHull
convexHull_subset_affineSpan 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.coe AffineSubspace addGroupIsAddTorsor AddCommGroup.toAddGroup AffineSubspace.instSetLike affineSpan	—	convexHull_min subset_affineSpan AffineSubspace.convex
convexHull_univ 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.univ	—	ClosureOperator.closure_top
convexHull_vadd 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Ring.toSemiring AddCommGroup.toAddCommMonoid HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor	—	AffineMap.image_convexHull
convexHull_zero 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Set.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	convexHull_singleton
convex_convexHull 📖	mathematical	—	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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	—	ClosureOperator.isClosed_closure
mem_convexHull_iff 📖	mathematical	—	Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	convexHull_eq_iInter
segment_subset_convexHull 📖	mathematical	Set Set.instMembership	Set Set.instHasSubset segment SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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	—	Convex.segment_subset convex_convexHull subset_convexHull
subset_convexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull	—	ClosureOperator.le_closure

---

← Back to Index