uniformity_basis_dist_pow — Mathlib

English

For a real r with 0 < r < 1, the entourages { (a,b) | dist(a,b) ≤ r^n } for n ∈ ℕ form a basis of the uniformity.

Русский

Пусть 0 < r < 1. Окружности { (a,b) | dist(a,b) ≤ r^n } для n∈ℕ образуют базис униформности.

LaTeX

$$$$ (\mathcal{U}(\alpha)) \HasBasis (n \in \mathbb{N}) \bigl( n \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) \le r^{n} \} \bigr) $$$$

Lean4

theorem uniformity_basis_dist_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => {p : α × α | dist p.1 p.2 < r ^ n} :=
  Metric.mk_uniformity_basis (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

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