uniformity_of_nhds_one_inv_mul — Mathlib

English

Using NHDS(1) with a basis (p,U), the uniformity has a basis of sets { (a,b) : a^{-1}b ∈ U_i }.

Русский

Используя базис NHDS(1) = (p,U), униформность имеет базис: { (a,b) : a^{-1}b ∈ U_i }.

LaTeX

$$$ (\\mathcal U(\\alpha)).HasBasis\\; p\\; i \\;\\{(x,y) : x^{-1}y \\in U_i\\} $$$

Lean4

@[to_additive]
theorem uniformity_of_nhds_one_inv_mul {ι} {p : ι → Prop} {U : ι → Set α} (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => {x : α × α | x.1⁻¹ * x.2 ∈ U i} :=
  by
  rw [uniformity_eq_comap_inv_mul_nhds_one]
  exact h.comap _

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