mem_closure_iff — Mathlib

English

Characterization of closure: a is in closure of s iff for every ε>0 there exists b∈s with dist(a,b)<ε.

Русский

Характеризация замыкания: a ∈ closure(s) тогда и только тогда, когда для каждого ε>0 найдётся b∈s такое, что dist(a,b)<ε.

LaTeX

$$$a \in \overline{s} \iff \forall \varepsilon>0, \exists b\in s, \operatorname{dist}(a,b) < \varepsilon$$$

Lean4

/-- ε-characterization of the closure in pseudometric spaces -/
theorem mem_closure_iff {s : Set α} {a : α} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_ball).trans <| by simp only [mem_ball, dist_comm]

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