mem_closure_iff — Mathlib

English

In a pseudo-emetric space, x lies in the closure of s if and only if for every ε > 0 there exists a point y ∈ s with edist(x, y) < ε.

Русский

В псевдоэмметрическом пространстве точка x принадлежит замыканию множества s тогда и только тогда, когда для любого ε > 0 существует y ∈ s such that edist(x, y) < ε.

LaTeX

$$$x \\in \\overline{s} \\iff \\forall \\varepsilon > 0, \\exists y \\in s, \\mathrm{edist}(x,y) < \\varepsilon$$$

Lean4

/-- ε-characterization of the closure in pseudoemetric spaces -/
theorem mem_closure_iff : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_eball).trans <| by simp only [mem_ball, edist_comm x]

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