English
For R a normed division ring and S a set of continuous linear maps, S is von Neumann bounded iff for every von Neumann bounded s ⊆ E, the image set { f(x) : f ∈ S, x ∈ s } is von Neumann bounded in F.
Русский
Для кольца R с нормированной структурой делимости и множества S непрерывных линейных отображений, S ограничено по Von Neumann ⇔ для каждого Von Neumann ограниченного s ⊆ E образ { f(x) : f ∈ S, x ∈ s } ограничен по Von Neumann в F.
LaTeX
$$$IsVonNBounded_R(S) \uiff \\forall s\\, IsVonNBounded_{𝕜_1}(s) \\, \\Rightarrow IsVonNBounded_R(\\mathrm{image2}(f,x \\mapsto f x) \\, S\\, s)$$$
Lean4
/-- A set `S` of continuous linear maps is von Neumann bounded
iff for any von Neumann bounded set `s`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.
For the forward implication with weaker typeclass assumptions, see `isVonNBounded_image2_apply`. -/
theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module R F]
[ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)} :
IsVonNBounded R S ↔ ∀ s, IsVonNBounded 𝕜₁ s → IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
UniformConvergenceCLM.isVonNBounded_iff
