uniformity_of_nhds_one — Mathlib

English

If a basis for 𝓝(1) is given by (p, U), then 𝓤(α) has a corresponding basis given by sets { (x,y) : y x^{-1} ∈ U_i }.

Русский

Если дан базис для 𝓝(1) в виде (p, U), то 𝓤(α) имеет соответствующий базис: { (x,y) : y x^{-1} ∈ U_i }.

LaTeX

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

Lean4

@[to_additive]
theorem uniformity_of_nhds_one {ι} {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_nhds_one]
  exact h.comap _

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