English
If s is closed and x ∉ convexHull 𝕜 s, then convexHull 𝕜 s is contained in the affine span of {x} together with those y ∈ s that are visible from x through convexHull 𝕜 s.
Русский
Если s замкнуто и x не лежит в выпуклой оболочке 𝕜 s, то выпуклая оболочка s лежит в аффинной оболочке множества {x} ∪ {y ∈ s | IsVisible 𝕜 (convexHull 𝕜 s) x y}.
LaTeX
$$$\text{convexHull } 𝕜 s \subseteq \operatorname{affineSpan}_{ℝ}({x}\cup\{y\in s\mid IsVisible 𝕜 (convexHull 𝕜 s) x y\})$$$
Lean4
/-- A set whose convex hull is closed lies in the cone based at a point `x` generated by its points
visible from `x` through its convex hull. -/
theorem convexHull_subset_affineSpan_isVisible (hs : IsClosed (convexHull ℝ s)) (hx : x ∉ convexHull ℝ s) :
convexHull ℝ s ⊆ affineSpan ℝ ({ x } ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) :=
by
rintro y hy
obtain ⟨z, hz, hxzy, hxz⟩ := hs.exists_wbtw_isVisible hy x
exact
AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
(affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <| hxz.mem_convexHull_isVisible hx hz)
(ne_of_mem_of_not_mem hz hx).symm
