mathlib documentation


Stone's separation theorem #

This file prove 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_convex_hull_triple {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {p q u v x y z : E} (hz : z ∈ segment π•œ x y) (hu : u ∈ segment π•œ x p) (hv : v ∈ segment π•œ y q) :
Β¬disjoint (segment π•œ u v) (⇑(convex_hull π•œ) {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} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {s t : set E} (hs : convex π•œ s) (ht : convex π•œ t) (hst : disjoint s t) :
βˆƒ (C : set E), convex π•œ C ∧ convex π•œ Cᢜ ∧ s βŠ† C ∧ t βŠ† Cᢜ

Stone's Separation Theorem