hasBasis_nhds_one_of_basis — Mathlib

English

If G is a uniform group, then UniformOnFun α G 𝔖 is a uniform group.

Русский

Если G — равномерная группа, то UniformOnFun α G 𝔖 — равномерная группа.

LaTeX

$$$\text{IsUniformGroup } G \rightarrow \text{IsUniformGroup } (\mathrm{UniformOnFun} \; α \; G \; 𝔖).$$$

Lean4

@[to_additive]
protected theorem hasBasis_nhds_one_of_basis {p : ι → Prop} {b : ι → Set G} (h : (𝓝 1 : Filter G).HasBasis p b) :
    (𝓝 1 : Filter (α →ᵤ G)).HasBasis p fun i => {f : α →ᵤ G | ∀ x, toFun f x ∈ b i} :=
  by
  convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one
  simp

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