Continuity and Von Neumann boundedness #
This file proves that for two topological vector spaces E and F over nontrivially normed fields,
if E is first countable, then every locally bounded linear map E →ₛₗ[σ] F is continuous
(this is LinearMap.continuous_of_locally_bounded).
References #
def
LinearMap.clmOfExistsBoundedImage
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
{F : Type u_4}
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[AddCommGroup F]
[TopologicalSpace F]
[NontriviallyNormedField 𝕜]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[NormedField 𝕜']
[Module 𝕜' F]
{σ : 𝕜 →+* 𝕜'}
[RingHomIsometric σ]
[IsTopologicalAddGroup F]
(f : E →ₛₗ[σ] F)
(h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V))
:
Construct a continuous linear map from a linear map f : E →ₛₗ[σ] F and the existence of a
neighborhood of zero that gets mapped into a bounded set in F.
Equations
- f.clmOfExistsBoundedImage h = { toLinearMap := f, cont := ⋯ }
Instances For
theorem
LinearMap.clmOfExistsBoundedImage_coe
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
{F : Type u_4}
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[AddCommGroup F]
[TopologicalSpace F]
[NontriviallyNormedField 𝕜]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[NormedField 𝕜']
[Module 𝕜' F]
{σ : 𝕜 →+* 𝕜'}
[RingHomIsometric σ]
[IsTopologicalAddGroup F]
{f : E →ₛₗ[σ] F}
{h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)}
:
@[simp]
theorem
LinearMap.clmOfExistsBoundedImage_apply
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
{F : Type u_4}
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[AddCommGroup F]
[TopologicalSpace F]
[NontriviallyNormedField 𝕜]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[NormedField 𝕜']
[Module 𝕜' F]
{σ : 𝕜 →+* 𝕜'}
[RingHomIsometric σ]
[IsTopologicalAddGroup F]
{f : E →ₛₗ[σ] F}
{h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)}
{x : E}
:
theorem
LinearMap.continuousAt_zero_of_locally_bounded
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
{F : Type u_4}
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[AddCommGroup F]
[TopologicalSpace F]
[NontriviallyNormedField 𝕜]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[NormedField 𝕜']
[Module 𝕜' F]
{σ : 𝕜 →+* 𝕜'}
[RingHomIsometric σ]
[FirstCountableTopology E]
(f : E →ₛₗ[σ] F)
(hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s))
:
ContinuousAt (⇑f) 0
theorem
LinearMap.continuous_of_locally_bounded
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
{F : Type u_4}
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[AddCommGroup F]
[TopologicalSpace F]
[NontriviallyNormedField 𝕜]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[NormedField 𝕜']
[Module 𝕜' F]
{σ : 𝕜 →+* 𝕜'}
[RingHomIsometric σ]
[FirstCountableTopology E]
[IsTopologicalAddGroup F]
(f : E →ₛₗ[σ] F)
(hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s))
:
Continuous ⇑f
If E is first countable, then every locally bounded linear map E →ₛₗ[σ] F is continuous.