English
If x is in the convex hull of s and y in convex hull of t, there exist x' ∈ s, y' ∈ t with dist x y ≤ dist x' y'.
Русский
Если x ∈ выпуклая оболочка s и y ∈ выпуклая оболочка t, найдутся x' ∈ s, y' ∈ t, такие что dist(x,y) ≤ dist(x',y').
LaTeX
$$∃ x'∈s ∃ y'∈t, dist x y ≤ dist x' y'$$
Lean4
/-- Given a point `x` in the convex hull of `s` and a point `y` in the convex hull of `t`,
there exist points `x' ∈ s` and `y' ∈ t` at distance at least `dist x y`. -/
theorem convexHull_exists_dist_ge2 {s t : Set E} {x y : E} (hx : x ∈ convexHull ℝ s) (hy : y ∈ convexHull ℝ t) :
∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y' :=
by
rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩
rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩
use x', hx', y', hy'
exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')
