theorem
Topology.IsInducing.isVonNBounded_iff
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedDivisionRing 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[(i : ι) → AddCommGroup (Eι i)]
[(i : ι) → Module 𝕜 (Eι i)]
[(i : ι) → TopologicalSpace (Eι i)]
{f : (i : ι) → E →ₗ[𝕜] Eι i}
[TopologicalSpace E]
(hf : IsInducing fun (x : E) (i : ι) => (f i) x)
(s : Set E)
:
If the topology on E is induced by a family of linear maps, then a set s : Set E is von
Neumann bounded if and only if its image under each map is von Neumann bounded.
theorem
Topology.IsInducing.isVonNBounded
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedDivisionRing 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[(i : ι) → AddCommGroup (Eι i)]
[(i : ι) → Module 𝕜 (Eι i)]
[(i : ι) → TopologicalSpace (Eι i)]
{f : (i : ι) → E →ₗ[𝕜] Eι i}
[TopologicalSpace E]
(hf : IsInducing fun (x : E) (i : ι) => (f i) x)
(s : Set E)
:
(∀ (i : ι), Bornology.IsVonNBounded 𝕜 (⇑(f i) '' s)) → Bornology.IsVonNBounded 𝕜 s
If the topology on E is induced by a family of linear maps, then a set s : Set E is von
Neumann bounded if its image under each map is von Neumann bounded.