uniformSpace — Mathlib

English

There is a UniformSpace structure on the space of linear maps E → SL[σ] F, induced by taking UniformConvergenceCLM on the coherent sets 𝔖.

Русский

Существуют равномерные структуры пространства линейных отображений E → SL[σ] F, индуцированные через UniformConvergenceCLM на когерентных множествах 𝔖.

LaTeX

$$$$ UniformSpace (E \to_{σ} F) $$$$

Lean4

instance uniformSpace [UniformSpace F] [IsUniformAddGroup F] : UniformSpace (E →SL[σ] F) :=
  UniformConvergenceCLM.instUniformSpace σ F {S | IsVonNBounded 𝕜₁ S}

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