convexHull_exists_dist_ge — Mathlib

English

Same as 55412 but with expanded quantifiers.

Русский

То же, что и в 55412, но с расширенными кванторами.

LaTeX

$$same as 55412$$

Lean4

/-- Given a point `x` in the convex hull of `s` and a point `y`, there exists a point
of `s` at distance at least `dist x y` from `y`. -/
theorem convexHull_exists_dist_ge {s : Set E} {x : E} (hx : x ∈ convexHull ℝ s) (y : E) :
    ∃ x' ∈ s, dist x y ≤ dist x' y :=
  (convexOn_dist y (convex_convexHull ℝ _)).exists_ge_of_mem_convexHull (subset_convexHull ..) hx

Похожие утверждения