uniformity_basis_dist_le_pow — Mathlib

English

For a real r with 0 < r < 1, the entourages { (a,b) | dist(a,b) ≤ r^n } (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}) (n \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) \le r^{n} \}). $$$$

Lean4

theorem uniformity_basis_dist_le_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_le (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

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