mem_closure_iff_infEdist_zero — Mathlib

English

x ∈ closure s iff infEdist x s = 0.

Русский

x принадлежит замыканию s тогда и только тогда, когда infEdist x s = 0.

LaTeX

$$$x \in \overline{s} \iff \infEdist x s = 0$$$

Lean4

/-- A point belongs to the closure of `s` iff its infimum edistance to this set vanishes -/
theorem mem_closure_iff_infEdist_zero : x ∈ closure s ↔ infEdist x s = 0 :=
  ⟨fun h => by
    rw [← infEdist_closure]
    exact infEdist_zero_of_mem h, fun h => EMetric.mem_closure_iff.2 fun ε εpos => infEdist_lt_iff.mp <| by rwa [h]⟩

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