English
Let E, F be normed spaces with the strong topology on CLM σ. Then the neighborhood of zero is the infimum over all von Neumann bounded s ⊆ E and all neighborhoods U of 0 in F of the principal sets {f : E →SL[σ] F | MapsTo f s U}. This describes 𝓝(0) in terms of bounded domain sets and target neighborhoods.
Русский
Для пространства непрерывных линейных отображений E →SL[σ] F в сильной топологии окрестность нуля задаётся как пересечение (наименьшая граница) по всем von Neumann ограниченным s ⊆ E и по всем окрестностям U числа 0 в F: 𝓝(0) = ⨅_{s} ⨅_{U∈𝓝0} 𝓟{f | MapsTo f s U}.
LaTeX
$$$\\\\mathcal{N}_0 = \\\\bigwedge_{s \\\\subset E, \\\\operatorname{IsVonNBounded}(s)} \\\\bigwedge_{U \\\\in \\\\mathcal{N}(0)} \\\\mathcal{P}\\\\{ f \\\\in E \\\\toSL[\\\\sigma] F \\\\mid MapsTo(f, s, U) \\\\}$$$
Lean4
protected theorem nhds_zero_eq [TopologicalSpace F] [IsTopologicalAddGroup F] :
𝓝 (0 : E →SL[σ] F) =
⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (U : Set F) (_ : U ∈ 𝓝 0), 𝓟 {f : E →SL[σ] F | MapsTo f s U} :=
UniformConvergenceCLM.nhds_zero_eq ..
