nhds_basis_ball_pow — Mathlib

English

In a metric space, for any point x and any radius r with 0 < r < 1, the neighborhoods of x have a basis consisting of the balls centered at x with radii r^n (n in N); i.e., the family { B(x, r^n) } forms a neighborhood basis at x.

Русский

В метрическом пространстве при 0 < r < 1 семейство шаров B(x, r^n) образует базис окрестностей точки x.

LaTeX

$$$(\mathcal{N}(x))$ имеет базис $\{ B(x, r^n) : n \in \mathbb{N} \}$, где $0 < r < 1$.$$

Lean4

theorem nhds_basis_ball_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => ball x (r ^ n) :=
  nhds_basis_uniformity (uniformity_basis_dist_pow h0 h1)

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