# Documentation

Mathlib.Analysis.Convex.Independent

# Convex independence #

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 #

• ConvexIndependent 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.
• convexIndependent_iff_finset: Carathéodory's theorem allows us to only check finsets to conclude convex independence.
• Convex.convexIndependent_extremePoints: Extreme points of a convex set are convex independent.
• https://en.wikipedia.org/wiki/Convex_position

## TODO #

Prove AffineIndependent.convexIndependent. This requires some glue between affineCombination and Finset.centerMass.

## Tags #

independence, convex position