52 Convex and discrete geometry

TheoremHelly's theorem #

Helly's theorem for finite families of convex sets in its classical form.

If F is a family of n convex sets in a vector space of finite dimension d, with n ≥ d + 1, and any d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

Convex.helly_theorem.{u_1, u_2, u_3} {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜]
  [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [_root_.Module 𝕜 E]
  [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι} (h_card : Module.finrank 𝕜 E + 1 ≤ s.card)
  (h_convex : ∀ i ∈ s, Convex 𝕜 (F i))
  (h_inter : ∀ I ⊆ s, I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
  (⋂ i ∈ s, F i).Nonempty

Sources

MathlibConvex.helly_theorem

Uses 7

Statement usesCardinal · Convex subsets · Field · Finite-dimensionality · Linear independence

Proof usesEuclidean domain · Radon's theorem

TheoremKrein–Milman theorem #

Krein-Milman theorem: In an LCTVS, any compact convex set is the closure of the convex hull of its extreme points.

closure_convexHull_extremePoints.{u_1} {E : Type u_1} [AddCommGroup E] [_root_.Module ℝ E]
  [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hAconv : Convex ℝ s) :
  closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s

Sources

Mathlibclosure_convexHull_extremePoints

Uses 14

Statement usesBornology · Closure · Compactness in terms of filters · Convex hull of a subset of an affine real space · Extreme point · Hausdorff space · Local convexity · Order · Topological module

Proof usesDual of a normed space · Extreme value theorem · Field \(\R\) of real numbers · Metric space · Ordered ring

TheoremRadon's theorem #

Radon's theorem on convex sets.

Any family f of affine dependent vectors contains a set I with the property that convex hulls of I and Iᶜ intersect nontrivially. In particular, any d + 2 points in a d-dimensional space can be partitioned this way, since they are affinely dependent (see finrank_vectorSpan_le_iff_not_affineIndependent).

Convex.radon_partition.{u_1, u_2, u_3} {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜]
  [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [_root_.Module 𝕜 E] {f : ι → E}
  (h : ¬AffineIndependent 𝕜 f) : ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty