uniformity_of_nhds_one_inv_mul_swapped

English

A swapped-inverse basis description: sets { (a,b): b^{-1}a ∈ U_i } generate 𝓤 α.

Русский

Описание базиса через обратную перестановку: множества { (a,b): b^{-1}a ∈ U_i } порождают 𝓤 α.

LaTeX

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

Lean4

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

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