Documentation Verification Report

Caratheodory

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

Statistics

Metric	Count
Definitions `minCardFinsetOfMemConvexHull`	1
Theorems `affineIndependent_minCardFinsetOfMemConvexHull`, `mem_convexHull_erase`, `mem_minCardFinsetOfMemConvexHull`, `minCardFinsetOfMemConvexHull_card_le_card`, `minCardFinsetOfMemConvexHull_nonempty`, `minCardFinsetOfMemConvexHull_subseteq`, `convexHull_eq_union`, `eq_pos_convex_span_of_mem_convexHull`	8
Total	9

Caratheodory

Definitions

Name	Category	Theorems
`minCardFinsetOfMemConvexHull` 📖	CompOp	5 math math: `minCardFinsetOfMemConvexHull_nonempty`, `minCardFinsetOfMemConvexHull_card_le_card`, `mem_minCardFinsetOfMemConvexHull`, `affineIndependent_minCardFinsetOfMemConvexHull`, `minCardFinsetOfMemConvexHull_subseteq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIndependent_minCardFinsetOfMemConvexHull` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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`	`AffineIndependent` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `minCardFinsetOfMemConvexHull`	—	`Finset.card_pos` `minCardFinsetOfMemConvexHull_nonempty` `mem_convexHull_erase` `mem_minCardFinsetOfMemConvexHull` `minCardFinsetOfMemConvexHull_card_le_card` `Set.Subset.trans` `Finset.erase_subset` `minCardFinsetOfMemConvexHull_subseteq` `not_lt` `Finset.card_erase_of_mem` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`mem_convexHull_erase` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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` `SetLike.coe`	`Finset.erase`	—	`Finset.convexHull_eq` `exists_nontrivial_relation_sum_zero_of_not_affine_ind` `Finset.exists_pos_of_sum_zero_of_exists_nonzero` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Finset.exists_min_image` `Finset.mem_filter` `Finset.filter_subset` `IsUnit.div_mul_cancel` `ne_of_gt` `sub_self` `Finset.insert_erase` `Finset.sum_insert` `Finset.notMem_erase` `zero_add` `Finset.sum_sub_distrib` `Finset.mul_sum` `MulZeroClass.mul_zero` `sub_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Finset.mem_of_subset` `le_of_lt` `Finset.centerMass_eq_of_sum_1` `Finset.sum_erase` `zero_smul` `Finset.sum_congr` `sub_smul` `SemigroupAction.mul_smul` `smul_zero` `inv_one` `one_smul`
`mem_minCardFinsetOfMemConvexHull` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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`	`SetLike.coe` `Finset` `Finset.instSetLike` `minCardFinsetOfMemConvexHull`	—	`instWellFoundedLTNat` `Function.argminOn_mem`
`minCardFinsetOfMemConvexHull_card_le_card` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `minCardFinsetOfMemConvexHull`	—	`Function.argminOn_le` `instWellFoundedLTNat` `Set.nonempty_of_mem`
`minCardFinsetOfMemConvexHull_nonempty` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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`	`Finset.Nonempty` `minCardFinsetOfMemConvexHull`	—	`Finset.coe_nonempty` `convexHull_nonempty_iff` `mem_minCardFinsetOfMemConvexHull`
`minCardFinsetOfMemConvexHull_subseteq` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `minCardFinsetOfMemConvexHull`	—	`instWellFoundedLTNat` `Function.argminOn_mem`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexHull_eq_union` 📖	mathematical	—	`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.iUnion` `Finset` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike` `AffineIndependent` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SetLike.instMembership`	—	`Set.Subset.antisymm` `Caratheodory.minCardFinsetOfMemConvexHull_subseteq` `Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull` `Caratheodory.mem_minCardFinsetOfMemConvexHull` `Set.iUnion_subset` `convexHull_mono`
`eq_pos_convex_span_of_mem_convexHull` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `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.instHasSubset` `Set.range` `AffineIndependent` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convexHull_eq_union` `Finset.convexHull_eq` `Subtype.range_coe_subtype` `Set.Subset.trans` `Finset.filter_subset` `AffineIndependent.comp_embedding` `Set.inclusion_injective` `LE.le.lt_of_ne` `Finset.mem_filter` `Finset.sum_congr` `Finset.sum_attach` `Finset.sum_filter_ne_zero` `Finset.sum_filter_of_ne` `zero_smul` `Finset.centerMass_eq_of_sum_1`

---

← Back to Index