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) :
Stone's Separation Theorem