English
If S is von Neumann bounded in the space of continuous linear maps and s is von Neumann bounded in the domain, then the set of all values {f(x) : f ∈ S, x ∈ s} is von Neumann bounded in the codomain with respect to the ring R.
Русский
Если S ограничено по von Neumann в пространстве непрерывных линейных отображений, а s ограничено по von Neumann в области, то множество всех значений { f(x) : f ∈ S, x ∈ s } ограничено по von Neumann в кодоманде относительно кольца R.
LaTeX
$$$IsVonNBounded_R(S) \\\\wedge IsVonNBounded_{\\\\mathbb{k}_1}(s) \\\\Rightarrow IsVonNBounded_R(\\\\{ f(x) \\\\mid f \\\\in S, x \\\\in s \\\\})$$$
Lean4
/-- If `S` is a von Neumann bounded set of continuous linear maps `f : E →SL[σ] F`
and `s` is a von Neumann bounded set in the domain,
then the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.
See also `isVonNBounded_iff` for an `Iff` version with stronger typeclass assumptions. -/
theorem isVonNBounded_image2_apply {R : Type*} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F]
[DistribMulAction R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)}
(hS : IsVonNBounded R S) {s : Set E} (hs : IsVonNBounded 𝕜₁ s) : IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
UniformConvergenceCLM.isVonNBounded_image2_apply hS hs
