theorem
Bornology.isVonNBounded_iff_of_iInf_induced
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[(i : ι) → AddCommGroup (Eι i)]
[(i : ι) → Module 𝕜 (Eι i)]
[(i : ι) → TopologicalSpace (Eι i)]
(f : (i : ι) → E →ₗ[𝕜] Eι i)
(s : Set E)
(hs : ∀ (i : ι), IsVonNBounded 𝕜 (⇑(f i) '' s))
:
IsVonNBounded 𝕜 s
theorem
Bornology.isVonNBounded_iff_of_iInf_induced'
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[(i : ι) → AddCommGroup (Eι i)]
[(i : ι) → Module 𝕜 (Eι i)]
[(i : ι) → TopologicalSpace (Eι i)]
(f : (i : ι) → E →ₗ[𝕜] Eι i)
(s : Set E)
(hs : ∀ (i : ι), IsVonNBounded 𝕜 (⇑(f i) '' s))
:
IsVonNBounded 𝕜 s
theorem
Topology.IsInducing.isVonNBounded
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedField 𝕜]
[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)
(hs : ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (⇑(f i) '' 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.
theorem
Topology.IsInducing.isVonNBounded_iff
{𝕜 : Type u_1}
{E : Type u_2}
{ι : Type u_3}
{Eι : ι → Type u_4}
[NormedField 𝕜]
[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.