instIsUniformAddGroup — Mathlib

English

The uniform structure on UniformConvergenceCLM σ F 𝔖 is defined so that the induced topology matches the underlying uniformity via the evaluation map.

Русский

Единая структура равномерности на UniformConvergenceCLM σ F 𝔖 задаётся так, что индуцированная топология совпадает с исходной равномерностью через отображение оценки.

LaTeX

$$$\\text{instUniformSpace}(\\sigma,F,\\mathcal{S}) :\\ UniformSpace (\\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}))$$$

Lean4

instance instIsUniformAddGroup [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖) :=
  by
  let φ : (UniformConvergenceCLM σ F 𝔖) →+ E →ᵤ[𝔖] F :=
    ⟨⟨(DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
  exact (isUniformEmbedding_coeFn _ _ _).isUniformAddGroup φ

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