nhds_basis_closed_eball — Mathlib

English

The neighborhood basis at x can be taken as closed balls with radii ε > 0.

Русский

Базис окрестностей в точке x может быть задан замкнутыми шарами радиуса ε > 0.

LaTeX

$$$ (\\mathcal{N}(x)) \\text{HasBasis} (\\lambda \\varepsilon. 0 < \\varepsilon) (\\mathrm{closedBall}(x)) $$$

Lean4

theorem nhds_basis_closed_eball : (𝓝 x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) (closedBall x) :=
  nhds_basis_uniformity uniformity_basis_edist_le

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