nhds_eq — Mathlib

English

The neighborhood filter at x equals the infimum of principal filters generated by balls around x with radii ε > 0.

Русский

Фильтр окрестностей в точке x равен инфимуму фундаментальных фильтров, порожденных шарами вокруг x радиуса ε > 0.

LaTeX

$$$\\mathcal{N}(x) = \\bigwedge_{\\varepsilon > 0} \\mathcal{P}(\\mathrm{ball}(x,\\varepsilon))$$$

Lean4

theorem nhds_eq : 𝓝 x = ⨅ ε > 0, 𝓟 (ball x ε) :=
  nhds_basis_eball.eq_biInf

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