nhds_basis_closedBall — Mathlib

English

A neighborhood basis at x can be taken as balls around x with radii 1/(n+1) for n ∈ ℕ.

Русский

Базис окрестностей точки x можно взять как шары вокруг x радиусов 1/(n+1), n ∈ ℕ.

LaTeX

$$$$ (\mathcal{N}(x)).HasBasis (n: \mathbb{N}) (\text{ball}(x, 1/(n+1))). $$$$

Lean4

theorem nhds_basis_closedBall : (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) (closedBall x) :=
  nhds_basis_uniformity uniformity_basis_dist_le

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