le_infDist — Mathlib

English

For any real r, r ≤ infDist x s holds exactly when every point y in s satisfies r ≤ dist(x, y), provided s is nonempty.

Русский

Для любого действительного r верно r ≤ infDist x s тогда и только тогда, когда для каждого y ∈ s выполняется r ≤ dist(x, y), при условии s непусто.

LaTeX

$$$\forall r\in\mathbb{R},\ s\neq\varnothing \Rightarrow (r \le \infDist x s) \iff (\forall y\in s,\ r \le \operatorname{dist}(x,y))$$$

Lean4

theorem le_infDist {r : ℝ} (hs : s.Nonempty) : r ≤ infDist x s ↔ ∀ ⦃y⦄, y ∈ s → r ≤ dist x y := by
  simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEdist_ne_top hs), le_infEdist,
    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]

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