Stone's separation theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
Stone's Separation Theorem
