infDist_lt_iff — Mathlib

English

The minimal distance to a nonempty set is strictly less than r if and only if there exists a point of the set within distance strictly less than r from x.

Русский

Минимальное расстояние до непустого множества строго меньше r тогда и только тогда существует точка y ∈ s с dist(x, y) < r.

LaTeX

$${r ∈ \mathbb{R}} (s \neq \varnothing) \Rightarrow (\infDist x s < r) \iff \exists y\in s, \ dist(x,y) < r$$

Lean4

/-- The minimal distance to a set `s` is `< r` iff there exists a point in `s` at distance `< r`. -/
theorem infDist_lt_iff {r : ℝ} (hs : s.Nonempty) : infDist x s < r ↔ ∃ y ∈ s, dist x y < r := by
  simp [← not_le, le_infDist hs]

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