English
All points y in the convex hull of s that are visible from x ∉ convexHull(s) lie in the convex hull of those visible points of s from x.
Русский
Каждая точка y в выпуклой оболочке s, которая видна из x, лежит в выпуклой оболочке множества точек s, которые видны из x.
LaTeX
$$$y\in convexHull\ 𝕜\ s \wedge x\notin convexHull\ 𝕜\ s \Rightarrow\ y\in convexHull\ {z\in s\mid IsVisible 𝕜 (convexHull 𝕜 s) x z}$$$
Lean4
/-- All points of the convex hull of a set `s` visible from a point `x ∉ convexHull ℝ s` lie in the
convex hull of such points that actually lie in `s`.
Note that the converse does not hold. -/
theorem mem_convexHull_isVisible (hx : x ∉ convexHull ℝ s) (hy : y ∈ convexHull ℝ s)
(hxy : IsVisible ℝ (convexHull ℝ s) x y) : y ∈ convexHull ℝ ({z ∈ s | IsVisible ℝ (convexHull ℝ s) x z}) := by
classical
obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
rw [← Fintype.sum_subset (s := {i | w i ≠ 0}) fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
exact
(convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero]) fun i hi ↦
subset_convexHull _ _
⟨ha _,
IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁ (by simpa) hx hxy (mem_univ _) <|
(hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩
