Independent

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

Statistics

Metric	Count
Definitions ConvexIndependent	1
Theorems convexIndependent_extremePoints, comp_embedding, injective, mem_convexHull_iff, mono, range, subtype, convexIndependent_iff_set, convexIndependent, convexIndependent_iff_finset, convexIndependent_iff_notMem_convexHull_diff, convexIndependent_set_iff_inter_convexHull_subset, convexIndependent_set_iff_notMem_convexHull_diff	13
Total	14

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexIndependent_extremePoints 📖	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	ConvexIndependent Set Set.instMembership Set.extremePoints	—	convexIndependent_set_iff_notMem_convexHull_diff extremePoints_convexHull_subset LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors inter_extremePoints_subset_extremePoints_of_subset convexHull_min HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset extremePoints_subset Set.mem_singleton

ConvexIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_embedding 📖	mathematical	ConvexIndependent	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Function.Injective.mem_set_image Function.Embedding.injective Set.image_image
injective 📖	—	ConvexIndependent	—	—	Set.image_singleton convexHull_singleton Set.mem_singleton
mem_convexHull_iff 📖	mathematical	ConvexIndependent	Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull AddCommGroup.toAddCommMonoid Set.image	—	subset_convexHull Set.mem_image_of_mem
mono 📖	—	ConvexIndependent Set Set.instMembership Set.instHasSubset	—	—	comp_embedding
range 📖	mathematical	ConvexIndependent	Set Set.instMembership Set.range	—	comp_embedding
subtype 📖	mathematical	ConvexIndependent	Set.Elem Set Set.instMembership	—	comp_embedding

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexIndependent_iff_set 📖	mathematical	—	ConvexIndependent Set Set.instMembership Set.range	—	ConvexIndependent.comp_embedding Set.mem_range_self ConvexIndependent.range

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexIndependent 📖	mathematical	—	ConvexIndependent	—	mem_iff_nonempty Set.image_nonempty convexHull_nonempty_iff

(root)

Definitions

Name	Category	Theorems
ConvexIndependent 📖	MathDef	7 math math: convexIndependent_set_iff_inter_convexHull_subset, Subsingleton.convexIndependent, convexIndependent_set_iff_notMem_convexHull_diff, Function.Injective.convexIndependent_iff_set, convexIndependent_iff_finset, Convex.convexIndependent_extremePoints, convexIndependent_iff_notMem_convexHull_diff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexIndependent_iff_finset 📖	mathematical	—	ConvexIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset Finset.instMembership	—	Finset.coe_image Finset.mem_singleton Finset.image_singleton Finset.coe_singleton convexHull_singleton Set.mem_singleton convexHull_eq_union_convexHull_finite_subsets Function.Injective.mem_set_image Function.Injective.injOn Finset.image_preimage Finset.filter_true_of_mem Set.image_subset_range Finset.mem_coe Finset.mem_preimage
convexIndependent_iff_notMem_convexHull_diff 📖	mathematical	—	ConvexIndependent Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull AddCommGroup.toAddCommMonoid Set.image Set.instSDiff Set.instSingletonSet	—	ConvexIndependent.mem_convexHull_iff Set.mem_singleton Set.diff_singleton_eq_self
convexIndependent_set_iff_inter_convexHull_subset 📖	mathematical	—	ConvexIndependent Set Set.instMembership Set.instHasSubset Set.instInter DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull AddCommGroup.toAddCommMonoid	—	Subtype.coe_image_of_subset Function.Injective.mem_set_image Subtype.coe_injective Subtype.coe_image_subset Subtype.prop
convexIndependent_set_iff_notMem_convexHull_diff 📖	mathematical	—	ConvexIndependent Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull AddCommGroup.toAddCommMonoid Set.instSDiff Set.instSingletonSet	—	convexIndependent_set_iff_inter_convexHull_subset Set.diff_subset Set.mem_singleton convexHull_mono Set.subset_diff_singleton

---

← Back to Index