instIsTopologicalAddGroup — Mathlib

English

If the target F is a T2 space and S is a cover of E, then UniformConvergenceCLM σ F 𝔖 is a T2 space as well.

Русский

Если F — пространство T2 и S покрытие E, то UniformConvergenceCLM σ F 𝔖 также является пространством T2.

LaTeX

$$$\\text{t2Space}(\\sigma,F,\\mathcal{S},h) :\\ T2Space \\big(\\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S})\\big)$$$

Lean4

instance instIsTopologicalAddGroup [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖) :=
  by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  infer_instance

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