convexOn_dist — Mathlib

English

Given x in convex hull of s and y in E, there exists x' in s with dist(x,y) ≤ dist(x',y).

Русский

Пусть x лежит в выпуклом замыкании s, а y произвольна. Тогда найдётся x' ∈ s такое, что dist(x,y) ≤ dist(x',y).

LaTeX

$$$\exists x'\in s:\ dist x y \le dist x' y$$$

Lean4

theorem convexOn_dist (z : E) (hs : Convex ℝ s) : ConvexOn ℝ s fun z' => dist z' z := by
  simpa [dist_eq_norm, preimage_preimage] using
    (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)

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