Topology of bounded convergence on the space of continuous linear map

In this file, we endow E →L[𝕜] F with the "topology of bounded convergence", or "topology of uniform convergence on bounded sets". This is declared as an instance.

A key feature of the topology of bounded convergence is that, in the normed setting, it coincides with the operator norm topology.

Note that, more generally, we defined the "topology of 𝔖-convergence" for any 𝔖 : Set (Set E) in Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM.

Here is a list of type aliases for E →L[𝕜] F endowed with various topologies :

• ContinuousLinearMap: topology of bounded convergence
• UniformConvergenceCLM: topology of 𝔖-convergence, for a general 𝔖 : Set (Set E)
• CompactConvergenceCLM: topology of compact convergence
• PointwiseConvergenceCLM: topology of pointwise convergence, also called "weak-* topology" or "strong-operator topology" depending on the context
• ContinuousLinearMapWOT: topology of weak pointwise convergence, also called "weak-operator topology"

Main definitions

• ContinuousLinearMap.topologicalSpace is the topology of bounded convergence. This is declared as an instance.

Main statements

• ContinuousLinearMap.topologicalAddGroup and ContinuousLinearMap.continuousSMul register these facts as instances for the special case of bounded convergence.

References

• N. Bourbaki, Topological Vector Spaces

Tags

uniform convergence, bounded convergence

Topology of bounded convergence

@[implicit_reducible]

instance ContinuousLinearMap.topologicalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : TopologicalSpace (E →SL[σ] F)

The topology of bounded convergence on E →L[𝕜] F. This coincides with the topology induced by the operator norm when E and F are normed spaces.

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousLinearMap.topologicalAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : IsTopologicalAddGroup (E →SL[σ] F)

instance ContinuousLinearMap.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SL[σ] F)

@[implicit_reducible]

instance ContinuousLinearMap.uniformSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] : UniformSpace (E →SL[σ] F)

Equations

• ContinuousLinearMap.uniformSpace = { toTopologicalSpace := ContinuousLinearMap.topologicalSpace, uniformity := UniformSpace.uniformity, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }

instance ContinuousLinearMap.isUniformAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] : IsUniformAddGroup (E →SL[σ] F)

instance ContinuousLinearMap.instContinuousEvalConst {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F

instance ContinuousLinearMap.instT2Space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] : T2Space (E →SL[σ] F)

theorem ContinuousLinearMap.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type u_7} {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set E × ι) => Bornology.IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun (Si : Set E × ι) => {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem ContinuousLinearMap.hasBasis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : (nhds 0).HasBasis (fun (SV : Set E × Set F) => Bornology.IsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}

theorem ContinuousLinearMap.isUniformEmbedding_toUniformOnFun {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] : IsUniformEmbedding fun (f : E →SL[σ] F) => (UniformOnFun.ofFun {s : Set E | Bornology.IsVonNBounded 𝕜₁ s}) ⇑f

instance ContinuousLinearMap.uniformContinuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [IsUniformAddGroup F] [UniformContinuousConstSMul M F] : UniformContinuousConstSMul M (E →SL[σ] F)

instance ContinuousLinearMap.continuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {M : Type u_7} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E →SL[σ] F)

theorem ContinuousLinearMap.nhds_zero_eq_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type u_7} {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : nhds 0 = ⨅ (s : Set E), ⨅ (_ : Bornology.IsVonNBounded 𝕜₁ s), ⨅ (i : ι), ⨅ (_ : p i), Filter.principal {f : E →SL[σ] F | Set.MapsTo (⇑f) s (b i)}

theorem ContinuousLinearMap.nhds_zero_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : nhds 0 = ⨅ (s : Set E), ⨅ (_ : Bornology.IsVonNBounded 𝕜₁ s), ⨅ U ∈ nhds 0, Filter.principal {f : E →SL[σ] F | Set.MapsTo (⇑f) s U}

theorem ContinuousLinearMap.eventually_nhds_zero_mapsTo {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] {s : Set E} (hs : Bornology.IsVonNBounded 𝕜₁ s) {U : Set F} (hu : U ∈ nhds 0) : ∀ᶠ (f : E →SL[σ] F) in nhds 0, Set.MapsTo (⇑f) s U

If s is a von Neumann bounded set and U is a neighbourhood of zero, then sufficiently small continuous linear maps map s to U.

theorem ContinuousLinearMap.isVonNBounded_image2_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {R : Type u_7} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [DistribMulAction R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)} (hS : Bornology.IsVonNBounded R S) {s : Set E} (hs : Bornology.IsVonNBounded 𝕜₁ s) : Bornology.IsVonNBounded R (Set.image2 (fun (f : E →SL[σ] F) (x : E) => f x) S s)

If S is a von Neumann bounded set of continuous linear maps f : E →SL[σ] F and s is a von Neumann bounded set in the domain, then the set {f x | (f ∈ S) (x ∈ s)} is von Neumann bounded.

See also isVonNBounded_iff for an Iff version with stronger typeclass assumptions.

theorem ContinuousLinearMap.isVonNBounded_iff {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] {R : Type u_7} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)} : Bornology.IsVonNBounded R S ↔ ∀ (s : Set E), Bornology.IsVonNBounded 𝕜₁ s → Bornology.IsVonNBounded R (Set.image2 (fun (f : E →SL[σ] F) (x : E) => f x) S s)

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 ContinuousLinearMap.completeSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] [ContinuousSMul 𝕜₁ E] (h : Topology.IsCoherentWith {s : Set E | Bornology.IsVonNBounded 𝕜₁ s}) : CompleteSpace (E →SL[σ] F)

instance ContinuousLinearMap.instCompleteSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E] [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] : CompleteSpace (E →SL[σ] F)

theorem ContinuousLinearMap.isUniformInducing_postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] [UniformSpace G] [IsUniformAddGroup G] (f : F →SL[τ] G) (hf : IsUniformInducing ⇑f) : IsUniformInducing f.comp

theorem ContinuousLinearMap.isUniformEmbedding_postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] [UniformSpace G] [IsUniformAddGroup G] (f : F →SL[τ] G) (hf : IsUniformEmbedding ⇑f) : IsUniformEmbedding f.comp

theorem ContinuousLinearMap.isInducing_postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] (f : F →SL[τ] G) (hf : Topology.IsInducing ⇑f) : Topology.IsInducing f.comp

theorem ContinuousLinearMap.isEmbedding_postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] (f : F →SL[τ] G) (hf : Topology.IsEmbedding ⇑f) : Topology.IsEmbedding f.comp

def ContinuousLinearMap.precomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) : (F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G

Pre-composition by a fixed continuous linear map as a continuous linear map.

Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.

Equations

• ContinuousLinearMap.precomp G L = { toFun := fun (f : F →SL[τ] G) => f.comp L, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.precomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) : (precomp G L) f = f.comp L

def ContinuousLinearMap.postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : (E →SL[σ] F) →SL[τ] E →SL[ρ] G

Post-composition by a fixed continuous linear map as a continuous linear map.

Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.

Equations

• ContinuousLinearMap.postcomp E L = { toFun := fun (f : E →SL[σ] F) => L.comp f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.postcomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) : (postcomp E L) f = L.comp f

theorem ContinuousLinearMap.toUniformConvergenceCLM_continuous {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_4} (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (𝔖 : Set (Set E)) (h : 𝔖 ⊆ {S : Set E | Bornology.IsVonNBounded 𝕜₁ S}) : Continuous ⇑(toUniformConvergenceCLM σ F 𝔖)

theorem ContinuousLinearMap.continuous_of_continuous_uncurry {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₂] [NormedField 𝕜₃] {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddCommGroup E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] {𝕜₁ : Type u_7} [NontriviallyNormedField 𝕜₁] {σ : 𝕜₁ →+* 𝕜₂} [Module 𝕜₁ E] {τ : 𝕜₃ →+* 𝕜₂} [RingHomSurjective τ] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (B : G →ₛₗ[τ] E →SL[σ] F) (hB : Continuous fun (p : G × E) => (B p.1) p.2) : Continuous ⇑B

A bilinear map B : E × F → G which is (jointly) continuous is hypocontinuous: in curried form, it defines a continuous linear map E →L[𝕜] F →L[𝕜] G.

In the normed setting, the converse is true, see ContinuousLinearMap.continuous₂. In general, however, hypocontinuity is a strictly weaker condition than joint continuity.

We prove some computation rules for continuous (semi-)bilinear maps in their first argument. If f is a continuous bilinear map, to use the corresponding rules for the second argument, use (f _).map_add and similar.

theorem ContinuousLinearMap.map_add₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x x' : E) (y : F) : (f (x + x')) y = (f x) y + (f x') y

theorem ContinuousLinearMap.map_zero₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (y : F) : (f 0) y = 0

theorem ContinuousLinearMap.map_smulₛₗ₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x : E) (y : F) : (f (c • x)) y = σ₁₃ c • (f x) y

def ContinuousLinearMap.toLinearMap₁₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G

Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity).

Equations

• L.toLinearMap₁₂ = ContinuousLinearMap.coeLMₛₗ σ₂₃ ∘ₛₗ ↑L

@[simp]

theorem ContinuousLinearMap.toLinearMap₁₂_apply {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) : (L.toLinearMap₁₂ v) w = (L v) w

theorem ContinuousLinearMap.toLinearMap₁₂_injective {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} : Function.Injective toLinearMap₁₂

theorem ContinuousLinearMap.toLinearMap₁₂_inj {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) : L₁.toLinearMap₁₂ = L₂.toLinearMap₁₂ ↔ L₁ = L₂

theorem ContinuousLinearMap.map_smul₂ {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommMonoid E] [Module 𝕜₃ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →L[𝕜₃] F →SL[σ₂₃] G) (c : 𝕜₃) (x : E) (y : F) : (f (c • x)) y = c • (f x) y

theorem ContinuousLinearMap.map_sub₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x x' : E) (y : F) : (f (x - x')) y = (f x) y - (f x') y

theorem ContinuousLinearMap.map_neg₂ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [Semiring R] [NormedField 𝕜₂] [NormedField 𝕜₃] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : (f (-x)) y = -(f x) y

def ContinuousLinearMap.toBilinForm {𝕜 : Type u_2} {E : Type u_5} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (L : E →L[𝕜] E →L[𝕜] 𝕜) : LinearMap.BilinForm 𝕜 E

Send a continuous bilinear form to an abstract bilinear form (forgetting continuity).

Equations

• L.toBilinForm = L.toLinearMap₁₂

@[simp]

theorem ContinuousLinearMap.toBilinForm_apply {𝕜 : Type u_2} {E : Type u_5} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (L : E →L[𝕜] E →L[𝕜] 𝕜) (v w : E) : (L.toBilinForm v) w = (L v) w

theorem ContinuousLinearMap.toBilinForm_injective {𝕜 : Type u_2} {E : Type u_5} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : Function.Injective toBilinForm

theorem ContinuousLinearMap.toBilinForm_inj {𝕜 : Type u_2} {E : Type u_5} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (L₁ L₂ : E →L[𝕜] E →L[𝕜] 𝕜) : L₁.toBilinForm = L₂.toBilinForm ↔ L₁ = L₂

theorem ContinuousLinearMap.isUniformEmbedding_restrictScalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsUniformEmbedding (restrictScalars 𝕜')

theorem ContinuousLinearMap.uniformContinuous_restrictScalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : UniformContinuous (restrictScalars 𝕜')

theorem ContinuousLinearMap.isEmbedding_restrictScalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Topology.IsEmbedding (restrictScalars 𝕜')

theorem ContinuousLinearMap.continuous_restrictScalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Continuous (restrictScalars 𝕜')

def ContinuousLinearMap.restrictScalarsL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] (F : Type u_3) [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] (𝕜'' : Type u_5) [Ring 𝕜''] [Module 𝕜'' F] [ContinuousConstSMul 𝕜'' F] [SMulCommClass 𝕜 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F] : (E →L[𝕜] F) →L[𝕜''] E →L[𝕜'] F

ContinuousLinearMap.restrictScalars as a ContinuousLinearMap.

Equations

• ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'' = { toLinearMap := ContinuousLinearMap.restrictScalarsₗ 𝕜 E F 𝕜' 𝕜'', cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] {𝕜' : Type u_4} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] {𝕜'' : Type u_5} [Ring 𝕜''] [Module 𝕜'' F] [ContinuousConstSMul 𝕜'' F] [SMulCommClass 𝕜 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F] : ↑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = restrictScalarsₗ 𝕜 E F 𝕜' 𝕜''

@[simp]

theorem ContinuousLinearMap.coe_restrict_scalarsL' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] {𝕜' : Type u_4} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] {𝕜'' : Type u_5} [Ring 𝕜''] [Module 𝕜'' F] [ContinuousConstSMul 𝕜'' F] [SMulCommClass 𝕜 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F] : ⇑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = restrictScalars 𝕜'

def ContinuousLinearMap.coprodEquivL {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [NormedField 𝕜] [Semiring S] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [Module S G] [SMulCommClass 𝕜 S G] [ContinuousConstSMul S G] : ((E →L[𝕜] G) × (F →L[𝕜] G)) ≃L[S] E × F →L[𝕜] G

ContinuousLinearMap.coprod as a ContinuousLinearEquiv.

Equations

• ContinuousLinearMap.coprodEquivL S = { toLinearEquiv := ContinuousLinearMap.coprodEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearMap.coprodEquivL_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [NormedField 𝕜] [Semiring S] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [Module S G] [SMulCommClass 𝕜 S G] [ContinuousConstSMul S G] (f : (E →L[𝕜] G) × (F →L[𝕜] G)) (a : E × F) : ((coprodEquivL S) f) a = f.1 a.1 + f.2 a.2

@[simp]

theorem ContinuousLinearMap.coprodEquivL_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [NormedField 𝕜] [Semiring S] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [Module S G] [SMulCommClass 𝕜 S G] [ContinuousConstSMul S G] (f : E × F →L[𝕜] G) : (coprodEquivL S).symm f = (f.comp (inl 𝕜 E F), f.comp (inr 𝕜 E F))

def ContinuousLinearMap.prodL {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [NormedField 𝕜] [Semiring S] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [Module S G] [SMulCommClass 𝕜 S G] [ContinuousConstSMul S G] [Module S F] [SMulCommClass 𝕜 S F] [ContinuousConstSMul S F] : ((E →L[𝕜] F) × (E →L[𝕜] G)) ≃L[S] E →L[𝕜] F × G

ContinuousLinearMap.prod as a ContinuousLinearEquiv.

Equations

• ContinuousLinearMap.prodL S = { toLinearEquiv := ContinuousLinearMap.prodₗ S, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearMap.prodL_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [NormedField 𝕜] [Semiring S] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [Module S G] [SMulCommClass 𝕜 S G] [ContinuousConstSMul S G] [Module S F] [SMulCommClass 𝕜 S F] [ContinuousConstSMul S F] (a✝ : (E →L[𝕜] F) × (E →L[𝕜] G)) : (prodL S) a✝ = a✝.1.prod a✝.2

def ContinuousLinearMap.toSpanSingletonCLE {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] : E ≃L[𝕜] 𝕜 →L[𝕜] E

ContinuousLinearMap.toSpanSingleton as a continuous linear equivalence.

Equations

• ContinuousLinearMap.toSpanSingletonCLE = { toLinearEquiv := ContinuousLinearMap.toSpanSingletonLE 𝕜 𝕜 E, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearMap.toSpanSingletonCLE_apply_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (x : E) (b : 𝕜) : (toSpanSingletonCLE x) b = b • x

@[simp]

theorem ContinuousLinearMap.toSpanSingletonCLE_symm_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (f : 𝕜 →L[𝕜] E) : toSpanSingletonCLE.symm f = f 1

Continuous linear equivalences

def ContinuousLinearEquiv.arrowCongrSL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G

A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) : (e₁₂.arrowCongrSL e₄₃) L = (↑e₄₃).comp (L.comp ↑e₁₂.symm)

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) : (e₁₂.arrowCongrSL e₄₃).toLinearEquiv L = (↑e₄₃).comp (L.comp ↑e₁₂.symm)

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) : (e₁₂.arrowCongrSL e₄₃).symm L = (↑e₄₃.symm).comp (L.comp ↑e₁₂)

@[simp]

theorem ContinuousLinearEquiv.arrowCongrSL_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) : (e₁₂.arrowCongrSL e₄₃).symm L = (↑e₄₃.symm).comp (L.comp ↑e₁₂)

def ContinuousLinearEquiv.arrowCongr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G

A pair of continuous linear equivalences generates a continuous linear equivalence between the spaces of continuous linear maps.

Equations

• e₁.arrowCongr e₂ = e₁.arrowCongrSL e₂

@[simp]

theorem ContinuousLinearEquiv.arrowCongr_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (f : E →L[𝕜] H) (x : F) : ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))

@[simp]

theorem ContinuousLinearEquiv.arrowCongr_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

def ContinuousLinearEquiv.conjContinuousAlgEquiv {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) : (G →L[𝕜] G) ≃A[𝕜] H →L[𝕜] H

A continuous linear equivalence of two spaces induces a continuous equivalence of algebras of their endomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : G →L[𝕜] G) (x : H) : (e.conjContinuousAlgEquiv f) x = e (f (e.symm x))

theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : H →L[𝕜] H) (x : G) : (e.conjContinuousAlgEquiv.symm f) x = e.symm (f (e x))

theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : G →L[𝕜] G) : e.conjContinuousAlgEquiv f = (↑e).comp (f.comp ↑e.symm)

@[simp]

theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) : e.conjContinuousAlgEquiv.symm = e.symm.conjContinuousAlgEquiv

@[simp]

theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_refl {𝕜 : Type u_1} {G : Type u_4} [AddCommGroup G] [NormedField 𝕜] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : (ContinuousLinearEquiv.refl 𝕜 G).conjContinuousAlgEquiv = ContinuousAlgEquiv.refl 𝕜 (G →L[𝕜] G)

theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_trans {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} {H : Type u_5} [AddCommGroup E] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] (e : E ≃L[𝕜] G) (f : G ≃L[𝕜] H) : (e.trans f).conjContinuousAlgEquiv = e.conjContinuousAlgEquiv.trans f.conjContinuousAlgEquiv