instLocallyConvexSpace — Mathlib

English

The space of continuous linear maps between modules, endowed with the uniform-convergence topology, is locally convex.

Русский

Пространство непрерывных линейных отображений между модулями, с топологией равномерной свертки, локально выпукло.

LaTeX

$$$\mathrm{LocallyConvexSpace}\;\mathsf{CLM}(E,F)$$$

Lean4

instance instLocallyConvexSpace : LocallyConvexSpace R (E →SL[σ] F) :=
  UniformConvergenceCLM.locallyConvexSpace R _ ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
    (directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union)

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