English
If a family of points indexed by a finite set is affine independent, then the convex hull of their intersection equals the intersection of their convex hulls.
Русский
Если множество точек аффинно независимо, то выпуклая оболочка их пересечения равна пересечению выпуклых оболочек.
LaTeX
$$$\operatorname{conv}(R, t_1 \cap t_2) = \operatorname{conv}(R, t_1) \cap \operatorname{conv}(R, t_2)$$$
Lean4
/-- Two simplices glue nicely if the union of their vertices is affine independent.
Note that `AffineIndependent.convexHull_inter` should be more versatile in most use cases. -/
theorem convexHull_inter' [DecidableEq E] (hs : AffineIndependent R ((↑) : ↑(t₁ ∪ t₂) → E)) :
convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂ :=
hs.convexHull_inter subset_union_left subset_union_right
