uniformity_basis_dist_rat — Mathlib

English

For a pseudo metric space α, the entourages { (a,b) | dist(a,b) < q } with rational q > 0 form a basis of the uniformity.

Русский

Пусть α — псевдометрическое пространство. Окружности { (a,b) | dist(a,b) < q } с рациональными q > 0 образуют базис униформности.

LaTeX

$$$$ (\mathcal{U}(\alpha)) \HasBasis (q \in \mathbb{Q}_{>0}) \bigl( q \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) < q \} \bigr) $$$$

Lean4

theorem uniformity_basis_dist_rat : (𝓤 α).HasBasis (fun r : ℚ => 0 < r) fun r => {p : α × α | dist p.1 p.2 < r} :=
  Metric.mk_uniformity_basis (fun _ => Rat.cast_pos.2) fun _ε hε =>
    let ⟨r, hr0, hrε⟩ := exists_rat_btwn hε
    ⟨r, Rat.cast_pos.1 hr0, hrε.le⟩

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