mem_closure_iff_ball — Mathlib

English

x ∈ closure s iff for every V ∈ 𝓤 α, (ball x V) ∩ s ≠ ∅.

Русский

x принадлежит замыканию s тогда и только тогда, когда для каждой V в 𝒰 α, шар вокруг x пересекает s.

LaTeX

$$$x \in \overline{s} \iff \forall V \in \mathcal U(\alpha), (\operatorname{ball}(x,V) \cap s).Nonempty$$$

Lean4

theorem mem_closure_iff_ball {s : Set α} {x} : x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty := by
  simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]

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