nhds_eq_uniformity — Mathlib

English

A basis-based formulation of closure via balls with symmetric, uniformity-bounded sets.

Русский

Базисная формулировка замыкания через шары с симметричными наборами равномерности.

LaTeX

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

Lean4

theorem nhds_eq_uniformity {x : α} : 𝓝 x = (𝓤 α).lift' (ball x) :=
  (nhds_basis_uniformity' (𝓤 α).basis_sets).eq_biInf

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