English
Either the convex hulls of s and t are disjoint, or their intersection is itself a convex hull of a face of K.
Русский
Либо выпуклые оболочки s и t не пересекаются, либо их пересечение является выпуклой оболочкой грани K.
LaTeX
$$$\\operatorname{Disjoint}(\\operatorname{convexHull} 𝕜 (s : Set E), \\operatorname{convexHull} 𝕜 ↑t) \\lor \\exists u \\in K.faces, \\operatorname{convexHull} 𝕜 (s : Set E) \\cap \\operatorname{convexHull} 𝕜 ↑t = \\operatorname{convexHull} 𝕜 ↑u$$$
Lean4
/-- The conclusion is the usual meaning of "glue nicely" in textbooks. It turns out to be quite
unusable, as it's about faces as sets in space rather than simplices. Further, additional structure
on `𝕜` means the only choice of `u` is `s ∩ t` (but it's hard to prove). -/
theorem disjoint_or_exists_inter_eq_convexHull (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
Disjoint (convexHull 𝕜 (s : Set E)) (convexHull 𝕜 ↑t) ∨
∃ u ∈ K.faces, convexHull 𝕜 (s : Set E) ∩ convexHull 𝕜 ↑t = convexHull 𝕜 ↑u :=
by
classical
by_contra! h
refine
h.2 (s ∩ t)
(K.down_closed hs inter_subset_left fun hst =>
h.1 <| disjoint_iff_inf_le.mpr <| (K.inter_subset_convexHull hs ht).trans ?_)
?_
· rw [← coe_inter, hst, coe_empty, convexHull_empty]
rfl
· rw [coe_inter, convexHull_inter_convexHull hs ht]
