mem_closure_iff_infDist_zero — Mathlib

English

x belongs to the closure of s if and only if infDist x s = 0 (assuming s nonempty).

Русский

x принадлежит замыканию s тогда и только тогда, когда infDist x s = 0 (при условии непустоты s).

LaTeX

$$$x \in closure(s) \iff infDist x s = 0 \quad (s \neq \varnothing)$$$

Lean4

/-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes. -/
theorem mem_closure_iff_infDist_zero (h : s.Nonempty) : x ∈ closure s ↔ infDist x s = 0 := by
  simp [mem_closure_iff_infEdist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEdist_ne_top h]

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