English
The image of a von Neumann bounded set under a continuous multilinear map is von Neumann bounded; this version requires the codomain to be a topological vector space.
Русский
Образ von Neumann ограниченного множества под непрерывным мультилинеарным отображением является ограниченным по фон Неймана; данная версия требует, чтобы кодовое пространство было топологическим линейным пространством.
LaTeX
$$IsVonNBounded 𝕜 (f '' s)$$
Lean4
/-- The image of a von Neumann bounded set under a continuous multilinear map
is von Neumann bounded.
This version assumes that the codomain is a topological vector space.
-/
theorem image_multilinear [ContinuousSMul 𝕜 F] {s : Set (∀ i, E i)} (hs : IsVonNBounded 𝕜 s)
(f : ContinuousMultilinearMap 𝕜 E F) : IsVonNBounded 𝕜 (f '' s) := by
cases isEmpty_or_nonempty ι with
| inl h =>
exact (isBounded_iff_isVonNBounded _).1 <| @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)
| inr h => exact hs.image_multilinear' f
