topologicalSpace — Mathlib

English

The map sending a uniform CLM to its UniformOnFun representation is an isometric uniform embedding.

Русский

Отображение, отправляющее UniformConvergenceCLM в его представление UniformOnFun, является изометричным вложением (uniform embedding).

LaTeX

$$$$ IsUniformEmbedding\left( f \mapsto UniformOnFun.ofFun\{s : \text{Bornology.IsVonNBounded } 𝕜_1 s\} f \right) $$$$

Lean4

/-- The topology of bounded convergence on `E →L[𝕜] F`. This coincides with the topology induced by
the operator norm when `E` and `F` are normed spaces. -/
instance topologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] : TopologicalSpace (E →SL[σ] F) :=
  UniformConvergenceCLM.instTopologicalSpace σ F {S | IsVonNBounded 𝕜₁ S}

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