English
Let E, F be normed spaces with a strong topology on the space of continuous linear maps E →SL[σ] F. If (p, b) is a basis of neighborhoods of 0 in F, then the neighborhood of 0 in the operator space is the greatest lower bound of all principal neighborhoods forcing each von Neumann bounded set s ⊆ E to be mapped into some basis neighborhood b i by every f in the map space, i.e. 𝓝0 = ⨅ s IsVonNBounded(s) ⨅ i (p i) 𝓟{ f : E →SL[σ] F | MapsTo f s (b i) }.
Русский
Пусть E, F — нормированные пространства, на множество непрерывно линейных отображений E →SL[σ] F действует сильная топология. Пусть (p, b) — база окрестностей нуля в F. Тогда окрестность нуля в пространстве отображений равна наименьшей сверху (наибольшей нижней границе) над всеми множествами, задающими ограниченность по von Neumann и содержащимися в базисных окрестностях: 𝓝0 = ⨅ s IsVonNBounded(s) ⨅ i p i 𝓟{ f : E →SL[σ] F | MapsTo f s (b i) }.
LaTeX
$$$\\\\mathcal{N}_0 = \\\\inf_{s \\\\subset E, \\, \\\\operatorname{IsVonNBounded}_{\\\\mathbb{K}_1}(s)} \\\\inf_{i \\\\in \\\\iota, \\, p(i)} \\\\mathcal{P}\\\\{ f : E \\\\toSL[\\\\sigma] F \\\\mid \\\\text{MapsTo}(f, s, b_i) \\\\}$$$
Lean4
protected theorem nhds_zero_eq_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} {p : ι → Prop}
{b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
𝓝 (0 : E →SL[σ] F) =
⨅ (s : Set E) (_ : IsVonNBounded 𝕜₁ s) (i : ι) (_ : p i), 𝓟 {f : E →SL[σ] F | MapsTo f s (b i)} :=
UniformConvergenceCLM.nhds_zero_eq_of_basis _ _ _ h
