Documentation

Mathlib.Analysis.Convex.StoneSeparation

Stone's separation theorem #

This file proves Stone's separation theorem. This tells us that any two disjoint convex sets can be separated by a convex set whose complement is also convex.

In locally convex real topological vector spaces, the Hahn-Banach separation theorems provide stronger statements: one may find a separating hyperplane, instead of merely a convex set whose complement is convex.

theorem not_disjoint_segment_convexHull_triple {๐•œ : Type u_1} {E : Type u_2} [LinearOrderedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : E} {q : E} {u : E} {v : E} {x : E} {y : E} {z : E} (hz : z โˆˆ segment ๐•œ x y) (hu : u โˆˆ segment ๐•œ x p) (hv : v โˆˆ segment ๐•œ y q) :
ยฌDisjoint (segment ๐•œ u v) (โ†‘(convexHull ๐•œ) {p, q, z})

In a tetrahedron with vertices x, y, p, q, any segment [u, v] joining the opposite edges [x, p] and [y, q] passes through any triangle of vertices p, q, z where z โˆˆ [x, y].

theorem exists_convex_convex_compl_subset {๐•œ : Type u_1} {E : Type u_2} [LinearOrderedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set E} {t : Set E} (hs : Convex ๐•œ s) (ht : Convex ๐•œ t) (hst : Disjoint s t) :
โˆƒ C, Convex ๐•œ C โˆง Convex ๐•œ Cแถœ โˆง s โŠ† C โˆง t โŠ† Cแถœ

Stone's Separation Theorem