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].