Topology of compact convergence on the space of continuous linear maps

In this file, we define a type alias CompactConvergenceCLM for E →L[𝕜] F, endowed with the topology of uniform convergence on compact subsets.

More concretely, CompactConvergenceCLM is an abbreviation for UniformConvergenceCLM σ F {(S : Set E) | IsCompact S}. We denote it by E →SL_c[σ] F.

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"

References

• N. Bourbaki, Topological Vector Spaces

Tags

uniform convergence, bounded convergence

Topology of compact convergence for continuous linear maps

@[reducible, inline]

abbrev CompactConvergenceCLM {𝕜₁ : 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] : Type (max u_4 u_5)

The topology of compact convergence on E →L[𝕜] F.

Equations

• CompactConvergenceCLM σ E F = UniformConvergenceCLM σ F {S : Set E | IsCompact S}

def CompactConvergenceCLM.«term_→SL_c[_]_» : Lean.TrailingParserDescr

The topology of compact convergence on E →L[𝕜] F.

Equations

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

def CompactConvergenceCLM.«term_→L_c[_]_» : Lean.TrailingParserDescr

The topology of compact convergence on E →L[𝕜] F.

Equations

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

instance CompactConvergenceCLM.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] [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (CompactConvergenceCLM σ E F)

instance CompactConvergenceCLM.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] : ContinuousEvalConst (CompactConvergenceCLM σ E F) E F

instance CompactConvergenceCLM.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] [T2Space F] : T2Space (CompactConvergenceCLM σ E F)

theorem CompactConvergenceCLM.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 × ι) => IsCompact Si.1 ∧ p Si.2) fun (Si : Set E × ι) => {f : CompactConvergenceCLM σ E F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem CompactConvergenceCLM.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) => IsCompact SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : CompactConvergenceCLM σ E F | ∀ x ∈ SV.1, f x ∈ SV.2}

def ContinuousLinearMap.precompCompactConvergenceCLM {𝕜₁ : 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] (L : E →SL[σ] F) : CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G

Specialization of ContinuousLinearMap.precomp_uniformConvergenceCLM to compact convergence.

Equations

• ContinuousLinearMap.precompCompactConvergenceCLM G L = ContinuousLinearMap.precompUniformConvergenceCLM G {S : Set E | IsCompact S} {S : Set F | IsCompact S} L ⋯

@[simp]

theorem ContinuousLinearMap.precompCompactConvergenceCLM_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] (L : E →SL[σ] F) (f : UniformConvergenceCLM τ G {S : Set F | IsCompact S}) : (precompCompactConvergenceCLM G L) f = comp f L

@[deprecated ContinuousLinearMap.precompCompactConvergenceCLM (since := "2026-01-27")]

def precomp_compactConvergenceCLM {𝕜₁ : 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] (L : E →SL[σ] F) : CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G

Alias of ContinuousLinearMap.precompCompactConvergenceCLM.

---

Specialization of ContinuousLinearMap.precomp_uniformConvergenceCLM to compact convergence.

Equations

• @precomp_compactConvergenceCLM = @ContinuousLinearMap.precompCompactConvergenceCLM

@[deprecated ContinuousLinearMap.precompCompactConvergenceCLM_apply (since := "2026-01-27")]

theorem precomp_compactConvergenceCLM_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] (L : E →SL[σ] F) (f : UniformConvergenceCLM τ G {S : Set F | IsCompact S}) : (ContinuousLinearMap.precompCompactConvergenceCLM G L) f = ContinuousLinearMap.comp f L

Alias of ContinuousLinearMap.precompCompactConvergenceCLM_apply.

def ContinuousLinearMap.postcompCompactConvergenceCLM {𝕜₁ : 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) : CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G

Specialization of ContinuousLinearMap.postcomp_uniformConvergenceCLM to compact convergence.

Equations

• ContinuousLinearMap.postcompCompactConvergenceCLM E L = ContinuousLinearMap.postcompUniformConvergenceCLM {S : Set E | IsCompact S} L

@[simp]

theorem ContinuousLinearMap.postcompCompactConvergenceCLM_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 : UniformConvergenceCLM σ F {S : Set E | IsCompact S}) : (postcompCompactConvergenceCLM E L) f = L.comp f

@[deprecated ContinuousLinearMap.postcompCompactConvergenceCLM (since := "2026-01-27")]

def postcomp_compactConvergenceCLM {𝕜₁ : 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) : CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G

Alias of ContinuousLinearMap.postcompCompactConvergenceCLM.

---

Specialization of ContinuousLinearMap.postcomp_uniformConvergenceCLM to compact convergence.

Equations

• @postcomp_compactConvergenceCLM = @ContinuousLinearMap.postcompCompactConvergenceCLM

@[deprecated ContinuousLinearMap.postcompCompactConvergenceCLM_apply (since := "2026-01-27")]

theorem postcomp_compactConvergenceCLM_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 : UniformConvergenceCLM σ F {S : Set E | IsCompact S}) : (ContinuousLinearMap.postcompCompactConvergenceCLM E L) f = L.comp f

Alias of ContinuousLinearMap.postcompCompactConvergenceCLM_apply.

Continuous linear equivalences

def CompactConvergenceCLM.piEquivL (𝕜₁ : Type u_1) [NormedField 𝕜₁] (E : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] {ι : Type u_7} (F : ι → Type u_8) [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜₁ (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)] : ((i : ι) → CompactConvergenceCLM (RingHom.id 𝕜₁) E (F i)) ≃L[𝕜₁] CompactConvergenceCLM (RingHom.id 𝕜₁) E ((i : ι) → F i)

ContinuousLinearMap.pi, upgraded to a continuous linear equivalence between Π i, E →L_c[𝕜] F i and E →L_c[𝕜] Π i, F i.

Equations

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

@[simp]

theorem CompactConvergenceCLM.piEquivL_apply {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_4} [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] {ι : Type u_7} (F : ι → Type u_8) [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜₁ (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)] (T : (i : ι) → CompactConvergenceCLM (RingHom.id 𝕜₁) E (F i)) (e : E) (i : ι) : ((piEquivL 𝕜₁ E F) T) e i = (T i) e

@[simp]

theorem CompactConvergenceCLM.piEquivL_symm_apply {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_4} [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] {ι : Type u_7} (F : ι → Type u_8) [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜₁ (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)] (T : CompactConvergenceCLM (RingHom.id 𝕜₁) E ((i : ι) → F i)) (e : E) (i : ι) : ((piEquivL 𝕜₁ E F).symm T i) e = T e i

def ContinuousLinearEquiv.compactConvergenceCLMCongrSL {𝕜 : Type u_7} {𝕜₂ : Type u_8} {𝕜₃ : Type u_9} {𝕜₄ : Type u_10} {E : Type u_11} {F : Type u_12} {G : Type u_13} {H : Type u_14} [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 σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : CompactConvergenceCLM σ₁₄ E H ≃SL[σ₄₃] CompactConvergenceCLM σ₂₃ F G

A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps. This version is for the type alias CompactConvergenceCLM.

Equations

• e₁₂.compactConvergenceCLMCongrSL e₄₃ = e₁₂.uniformConvergenceCLMCongrSL e₄₃ {S : Set E | IsCompact S} {S : Set F | IsCompact S} ⋯

@[simp]

theorem ContinuousLinearEquiv.compactConvergenceCLMCongrSL_apply {𝕜 : Type u_7} {𝕜₂ : Type u_8} {𝕜₃ : Type u_9} {𝕜₄ : Type u_10} {E : Type u_11} {F : Type u_12} {G : Type u_13} {H : Type u_14} [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 σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (φ : CompactConvergenceCLM σ₁₄ E H) (f : F) : ((e₁₂.compactConvergenceCLMCongrSL e₄₃) φ) f = e₄₃ (φ (e₁₂.symm f))

@[simp]

theorem ContinuousLinearEquiv.compactConvergenceCLMCongrSL_symm_apply {𝕜 : Type u_7} {𝕜₂ : Type u_8} {𝕜₃ : Type u_9} {𝕜₄ : Type u_10} {E : Type u_11} {F : Type u_12} {G : Type u_13} {H : Type u_14} [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 σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (φ : CompactConvergenceCLM σ₂₃ F G) (e : E) : ((e₁₂.compactConvergenceCLMCongrSL e₄₃).symm φ) e = e₄₃.symm (φ (e₁₂ e))

def ContinuousLinearEquiv.compactConvergenceCLMCongr {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [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) : CompactConvergenceCLM (RingHom.id 𝕜) E H ≃L[𝕜] CompactConvergenceCLM (RingHom.id 𝕜) F G

A pair of continuous linear equivalences generates a continuous linear equivalence between the spaces of continuous linear maps. This version is for the type alias CompactConvergenceCLM.

Equations

• e₁.compactConvergenceCLMCongr e₂ = e₁.compactConvergenceCLMCongrSL e₂

@[simp]

theorem ContinuousLinearEquiv.compactConvergenceCLMCongr_apply {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [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) (φ : CompactConvergenceCLM (RingHom.id 𝕜) E H) (f : F) : ((e₁.compactConvergenceCLMCongr e₂) φ) f = e₂ (φ (e₁.symm f))

@[simp]

theorem ContinuousLinearEquiv.compactConvergenceCLMCongr_symm_apply {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [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) (φ : CompactConvergenceCLM (RingHom.id 𝕜) F G) (e : E) : ((e₁.compactConvergenceCLMCongr e₂).symm φ) e = e₂.symm (φ (e₁ e))