mem_closure_iff — Mathlib

English

For any set s ⊆ ℝ, x ∈ closure s iff ∀ ε>0 ∃ y∈s with |y−x|<ε.

Русский

Для любого множества s ⊆ ℝ верно: x ∈ замыкание s тогда и только тогда, когда ∀ε>0 существует y∈s такое что |y−x|<ε.

LaTeX

$$$x \in \overline{s} \iff \forall \varepsilon>0, \exists y\in s, |y-x|<\varepsilon$$$

Lean4

theorem mem_closure_iff {s : Set ℝ} {x : ℝ} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε := by
  simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]

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