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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup 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) ((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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup 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