not_disjoint_segment_convexHull_triple
theorem not_disjoint_segment_convexHull_triple :
β {π : Type u_1} {E : Type u_2} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{p q u v x y z : E},
z β segment π x y β
u β segment π x p β v β segment π y q β Β¬Disjoint (segment π u v) ((convexHull π) {p, q, z})
In a three-dimensional space, given a tetrahedron with vertices `x`, `y`, `p`, `q`, a segment `[u, v]` that joins the opposite edges `[x, p]` and `[y, q]`, and a triangle formed by the vertices `p`, `q`, and `z` where `z` lies on the line segment `[x, y]`, this theorem states that the segment `[u, v]` is not disjoint from the convex hull of the triangle `{p, q, z}`. In other words, the line segment `[u, v]` must intersect or pass through the interior of the triangle `{p, q, z}`.
More concisely: Given a tetrahedron in three-dimensional space with opposite edges [x, p] and [y, q], and a triangle with vertices p, q, and z on the line segment [x, y], the segment [u, v] joining the edges [x, p] and [y, q] intersects or lies in the convex hull of {p, q, z}.
|
exists_convex_convex_compl_subset
theorem exists_convex_convex_compl_subset :
β {π : Type u_1} {E : Type u_2} [inst : LinearOrderedField π] [inst_1 : AddCommGroup E] [inst_2 : Module π E]
{s t : Set E}, Convex π s β Convex π t β Disjoint s t β β C, Convex π C β§ Convex π CαΆ β§ s β C β§ t β CαΆ
**Stone's Separation Theorem** states that for any linearly ordered field `π` and an additively commutative group `E` that is a module over `π`, given two disjoint convex sets `s` and `t`, there exists another convex set `C` such that `s` is a subset of `C` and `t` is a subset of the complement of `C`. Furthermore, the complement of `C` is also convex. In simpler terms, Stone's Separation Theorem guarantees the existence of a "dividing line" (the set `C`) between two disjoint convex sets in a vector space.
More concisely: Given a linearly ordered field `π` and an additively commutative `π`-module `E`, for any two disjoint convex sets `s` and `t` in `E`, there exists a convex set `C` such that `s β C` and `t β E \ C`.
|