English
If S is von Neumann bounded in the operator space and s ⊆ E is von Neumann bounded, then for any neighborhood U of 0 in F there exists a neighborhood of 0 in the operator space such that every f in that neighborhood maps s into U, i.e., eventually MapsTo f s U holds along 𝓝0.
Русский
Если S ограничено по von Neumann в пространстве линейных отображений и s ⊆ E ограничено, то для любого окрестного нуля U в F существует окрестность нуля в пространстве линейных отображений, такая что каждый f в этой окрестности отображает s в U; т.е. выполняется eventually MapsTo f s U
LaTeX
$$$\\\\text{IsVonNBounded}_R(S) \u2192 \\\\forall U \\\\(U \u2208 𝓝 0) \\\\exists V \\in 𝓝 0 \\, (\\\\forall f \\in V, MapsTo(f, s, U))$$$
Lean4
/-- If `s` is a von Neumann bounded set and `U` is a neighbourhood of zero,
then sufficiently small continuous linear maps map `s` to `U`. -/
theorem eventually_nhds_zero_mapsTo [TopologicalSpace F] [IsTopologicalAddGroup F] {s : Set E} (hs : IsVonNBounded 𝕜₁ s)
{U : Set F} (hu : U ∈ 𝓝 0) : ∀ᶠ f : E →SL[σ] F in 𝓝 0, MapsTo f s U :=
UniformConvergenceCLM.eventually_nhds_zero_mapsTo _ hs hu
