Convex independence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines convex independent families of points.
Convex independence is closely related to affine independence. In both cases, no point can be written as a combination of others. When the combination is affine (that is, any coefficients), this yields affine independence. When the combination is convex (that is, all coefficients are nonnegative), then this yields convex independence. In particular, affine independence implies convex independence.
Main declarations #
convex_independent p: Convex independence of the indexed family
p : ι → E. Every point of the family only belongs to convex hulls of sets of the family containing it.
convex_independent_iff_finset: Carathéodory's theorem allows us to only check finsets to conclude convex independence.
convex.extreme_points_convex_independent: Extreme points of a convex set are convex independent.
affine_independent.convex_independent. This requires some glue between
independence, convex position
An indexed family is said to be convex independent if every point only belongs to convex hulls of sets containing it.
- convex_independent 𝕜 p = ∀ (s : set ι) (x : ι), p x ∈ ⇑(convex_hull 𝕜) (p '' s) → x ∈ s
A family with at most one point is convex independent.
A convex independent family is injective.
If a family is convex independent, so is any subfamily given by composition of an embedding into index type with the original family.
If a family is convex independent, so is any subfamily indexed by a subtype of the index type.
If an indexed family of points is convex independent, so is the corresponding set of points.
A subset of a convex independent set of points is convex independent as well.
The range of an injective indexed family of points is convex independent iff that family is.
If a family is convex independent, a point in the family is in the convex hull of some of the points given by a subset of the index type if and only if the point's index is in this subset.
If a family is convex independent, a point in the family is not in the convex hull of the other
convex_independent_set_iff_not_mem_convex_hull_diff for the
If a set is convex independent, a point in the set is not in the convex hull of the other
convex_independent_iff_not_mem_convex_hull_diff for the indexed family version.
To check convex independence, one only has to check finsets thanks to Carathéodory's theorem.