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	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	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	114 math math: convexIndependent_set_iff_inter_convexHull_subset, IsLinearMap.image_convexHull, convexHull_insert, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, 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, convexJoin_segments, convexHull_union_neg_eq_absConvexHull, interior_convexHull_nonempty_iff_affineSpan_eq_top, 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, Convex.mem_extremePoints_iff_mem_diff_convexHull_diff, 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, 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, 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, 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, AffineIndependent.convexHull_inter, Set.Finite.convexHull_eq, 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	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	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.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