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 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_iff_notMem_convexHull_diff extremePoints_convexHull_subset LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE 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	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 📖	mathematical	ConvexIndependent Set Set.instMembership Set.instHasSubset	ConvexIndependent Set Set.instMembership	—	comp_embedding
range 📖	mathematical	ConvexIndependent	ConvexIndependent Set Set.instMembership Set.range	—	comp_embedding
subtype 📖	mathematical	ConvexIndependent	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	11 math math: convexIndependent_set_iff_inter_convexHull_subset, ConvexIndependent.mono, Subsingleton.convexIndependent, ConvexIndependent.comp_embedding, convexIndependent_set_iff_notMem_convexHull_diff, Function.Injective.convexIndependent_iff_set, convexIndependent_iff_finset, ConvexIndependent.range, ConvexIndependent.subtype, 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 SetLike.instMembership Finset.instSetLike	—	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