infEdist_lt_iff — Mathlib

English

The edistance to a set is less than r iff there exists a point in the set at edistance less than r.

Русский

Расстояние до множества меньше r тогда и только тогда, когда существует точка в множестве на расстоянии меньше r.

LaTeX

$$$\infEdist x s < r \iff \exists y \in s\, edist x y < r$$$

Lean4

/-- The edist to a set is `< r` iff there exists a point in the set at edistance `< r` -/
theorem infEdist_lt_iff {r : ℝ≥0∞} : infEdist x s < r ↔ ∃ y ∈ s, edist x y < r := by
  simp_rw [infEdist, iInf_lt_iff, exists_prop]

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