hasBasis_uniformity — Mathlib

English

The uniformity 𝒰_R has a basis given by γ ∈ Γ₀ˣ with the sets { (p, q) ∈ R×R : v(q − p) < γ }.

Русский

Унитизация 𝒰_R имеет базис, заданный γ ∈ Γ₀ˣ, множествами { (p, q) ∈ R×R : v(q − p) < γ }.

LaTeX

$$$\mathcal{U}_R \text{ has basis } γ: Γ_0^{\times}, \{(p,q)\in R\times R : v(q-p) < γ\}$$$

Lean4

theorem hasBasis_uniformity : (𝓤 R).HasBasis (fun _ => True) fun γ : Γ₀ˣ => {p : R × R | v (p.2 - p.1) < (γ : Γ₀)} :=
  by
  rw [uniformity_eq_comap_nhds_zero]
  exact (hasBasis_nhds_zero R Γ₀).comap _

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