Strong topologies on the space of continuous linear maps

In this file, we define the strong topologies on E →L[𝕜] F associated with a family 𝔖 : Set (Set E) to be the topology of uniform convergence on the elements of 𝔖 (also called the topology of 𝔖-convergence).

The lemma UniformOnFun.continuousSMul_of_image_bounded tells us that this is a vector space topology if the continuous linear image of any element of 𝔖 is bounded (in the sense of Bornology.IsVonNBounded).

We then declare an instance for the case where 𝔖 is exactly the set of all bounded subsets of E, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of bounded convergence"), which coincides with the operator norm topology in the case of NormedSpaces.

Other useful examples include the weak-* topology (when 𝔖 is the set of finite sets or the set of singletons) and the topology of compact convergence (when 𝔖 is the set of relatively compact sets).

Main definitions

• UniformConvergenceCLM is a type synonym for E →SL[σ] F equipped with the 𝔖-topology.
• UniformConvergenceCLM.instTopologicalSpace is the topology mentioned above for an arbitrary 𝔖.
• ContinuousLinearMap.topologicalSpace is the topology of bounded convergence. This is declared as an instance.

Main statements

• UniformConvergenceCLM.instTopologicalAddGroup and UniformConvergenceCLM.instContinuousSMul show that the strong topology makes E →L[𝕜] F a topological vector space, with the assumptions on 𝔖 mentioned above.
• ContinuousLinearMap.topologicalAddGroup and ContinuousLinearMap.continuousSMul register these facts as instances for the special case of bounded convergence.

References

• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

TODO

• Add convergence on compact subsets

Tags

uniform convergence, bounded convergence

𝔖-Topologies

def UniformConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] : Set (Set E) → Type (max u_3 u_4)

Given E and F two topological vector spaces and 𝔖 : Set (Set E), then UniformConvergenceCLM σ F 𝔖 is a type synonym of E →SL[σ] F equipped with the "topology of uniform convergence on the elements of 𝔖".

If the continuous linear image of any element of 𝔖 is bounded, this makes E →SL[σ] F a topological vector space.

Equations

• UniformConvergenceCLM σ F x = (E →SL[σ] F)

instance UniformConvergenceCLM.instFunLike {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] (𝔖 : Set (Set E)) : FunLike (UniformConvergenceCLM σ F 𝔖) E F

Equations

• UniformConvergenceCLM.instFunLike σ F 𝔖 = ContinuousLinearMap.funLike

instance UniformConvergenceCLM.instContinuousSemilinearMapClass {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] (𝔖 : Set (Set E)) : ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F

Equations

• ⋯ = ⋯

instance UniformConvergenceCLM.instTopologicalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalSpace (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖)

theorem UniformConvergenceCLM.topologicalSpace_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

instance UniformConvergenceCLM.instUniformSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformSpace (UniformConvergenceCLM σ F 𝔖)

The uniform structure associated with ContinuousLinearMap.strongTopology. We make sure that this has nice definitional properties.

Equations

• UniformConvergenceCLM.instUniformSpace σ F 𝔖 = (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).replaceTopology ⋯

theorem UniformConvergenceCLM.uniformSpace_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformConvergenceCLM.instUniformSpace σ F 𝔖 = UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)

@[simp]

theorem UniformConvergenceCLM.uniformity_toTopologicalSpace_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformSpace.toTopologicalSpace = UniformConvergenceCLM.instTopologicalSpace σ F 𝔖

theorem UniformConvergenceCLM.isUniformInducing_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

theorem UniformConvergenceCLM.isUniformEmbedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

@[deprecated UniformConvergenceCLM.isUniformEmbedding_coeFn]

theorem UniformConvergenceCLM.uniformEmbedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

Alias of UniformConvergenceCLM.isUniformEmbedding_coeFn.

theorem UniformConvergenceCLM.isEmbedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : IsEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

@[deprecated UniformConvergenceCLM.isEmbedding_coeFn]

theorem UniformConvergenceCLM.embedding_coeFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : IsEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

Alias of UniformConvergenceCLM.isEmbedding_coeFn.

instance UniformConvergenceCLM.instAddCommGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : AddCommGroup (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instAddCommGroup σ F 𝔖 = ContinuousLinearMap.addCommGroup

@[simp]

theorem UniformConvergenceCLM.coe_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : ⇑0 = 0

instance UniformConvergenceCLM.instUniformAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : UniformAddGroup (UniformConvergenceCLM σ F 𝔖)

Equations

• ⋯ = ⋯

instance UniformConvergenceCLM.instTopologicalAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)

Equations

• ⋯ = ⋯

theorem UniformConvergenceCLM.continuousEvalConst {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) : ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F

theorem UniformConvergenceCLM.t2Space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] [T2Space F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) : T2Space (UniformConvergenceCLM σ F 𝔖)

instance UniformConvergenceCLM.instDistribMulAction {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] (M : Type u_5) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : DistribMulAction M (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instDistribMulAction σ F M 𝔖 = ContinuousLinearMap.distribMulAction

instance UniformConvergenceCLM.instModule {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] (R : Type u_5) [Semiring R] [Module R F] [SMulCommClass 𝕜₂ R F] [TopologicalSpace F] [ContinuousConstSMul R F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : Module R (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instModule σ F R 𝔖 = ContinuousLinearMap.module

theorem UniformConvergenceCLM.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E)) (h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S) : ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

theorem UniformConvergenceCLM.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] {ι : Type u_5} (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) 𝔖) {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set E × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set E × ι) => {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem UniformConvergenceCLM.hasBasis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) 𝔖) : (nhds 0).HasBasis (fun (SV : Set E × Set F) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2}

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

theorem UniformConvergenceCLM.nhds_zero_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : nhds 0 = ⨅ s ∈ 𝔖, ⨅ t ∈ nhds 0, Filter.principal {f : UniformConvergenceCLM σ F 𝔖 | Set.MapsTo (⇑f) s t}

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

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

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

A set S of continuous linear maps with topology of uniform convergence on sets s ∈ 𝔖 is von Neumann bounded iff for any s ∈ 𝔖, the set {f x | (f ∈ S) (x ∈ s)} is von Neumann bounded.

instance UniformConvergenceCLM.instUniformContinuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] (M : Type u_5) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) : UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

Equations

• ⋯ = ⋯

instance UniformConvergenceCLM.instContinuousConstSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] (M : Type u_5) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

Equations

• ⋯ = ⋯

theorem UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] {ι : Type u_5} {p : Filter ι} [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖} {a₀ : UniformConvergenceCLM σ F 𝔖} : Filter.Tendsto a p (nhds a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun (x1 : ι) (x2 : E) => (a x1) x2) (⇑a₀) p s

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

theorem UniformConvergenceCLM.completeSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] {𝔖 : Set (Set E)} (h𝔖 : RestrictGenTopology 𝔖) (h𝔖U : ⋃₀ 𝔖 = Set.univ) : CompleteSpace (UniformConvergenceCLM σ F 𝔖)

theorem UniformConvergenceCLM.uniformSpace_mono {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] {𝔖₁ : Set (Set E)} {𝔖₂ : Set (Set E)} [UniformSpace F] [UniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) : UniformConvergenceCLM.instUniformSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instUniformSpace σ F 𝔖₂

theorem UniformConvergenceCLM.topologicalSpace_mono {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] {𝔖₁ : Set (Set E)} {𝔖₂ : Set (Set E)} [TopologicalSpace F] [TopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) : UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₂

Topology of bounded convergence

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] [TopologicalAddGroup 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

• ContinuousLinearMap.topologicalSpace = UniformConvergenceCLM.instTopologicalSpace σ F {S : Set E | Bornology.IsVonNBounded 𝕜₁ S}

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] [TopologicalAddGroup F] : TopologicalAddGroup (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [UniformAddGroup F] : UniformSpace (E →SL[σ] F)

Equations

• ContinuousLinearMap.uniformSpace = UniformConvergenceCLM.instUniformSpace σ F {S : Set E | Bornology.IsVonNBounded 𝕜₁ S}

instance ContinuousLinearMap.uniformAddGroup {𝕜₁ : 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] [UniformAddGroup F] : UniformAddGroup (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] : T2Space (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [UniformAddGroup F] : IsUniformEmbedding fun (f : E →SL[σ] F) => (UniformOnFun.ofFun {s : Set E | Bornology.IsVonNBounded 𝕜₁ s}) ⇑f

@[deprecated ContinuousLinearMap.isUniformEmbedding_toUniformOnFun]

theorem ContinuousLinearMap.uniformEmbedding_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] [UniformAddGroup F] : IsUniformEmbedding fun (f : E →SL[σ] F) => (UniformOnFun.ofFun {s : Set E | Bornology.IsVonNBounded 𝕜₁ s}) ⇑f

Alias of ContinuousLinearMap.isUniformEmbedding_toUniformOnFun.

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] [UniformAddGroup F] [UniformContinuousConstSMul M F] : UniformContinuousConstSMul M (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E →SL[σ] F)

Equations

• ⋯ = ⋯

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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] [TopologicalAddGroup F] [Module 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] [TopologicalAddGroup 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] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] [ContinuousSMul 𝕜₁ E] (h : RestrictGenTopology {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] [TopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E] [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] : CompleteSpace (E →SL[σ] F)

Equations

• ⋯ = ⋯

@[simp]

theorem ContinuousLinearMap.precomp_toFun {𝕜₁ : 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] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) : (ContinuousLinearMap.precomp G L) f = f.comp L

@[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] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ] [RingHomIsometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) : (ContinuousLinearMap.precomp G L) f = f.comp L

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] [TopologicalAddGroup 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.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] [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) : (ContinuousLinearMap.postcomp E L) f = L.comp f

@[simp]

theorem ContinuousLinearMap.postcomp_toFun {𝕜₁ : 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] [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) : (ContinuousLinearMap.postcomp E L) f = L.comp f

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] [TopologicalAddGroup F] [TopologicalAddGroup 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 := ⋯ }

def ContinuousLinearMap.toLinearMap₂ {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) : E →ₗ[𝕜] F →ₗ[𝕜] G

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

Equations

• L.toLinearMap₂ = ContinuousLinearMap.coeLM 𝕜 ∘ₗ ↑L

@[simp]

theorem ContinuousLinearMap.toLinearMap₂_apply {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) (v : E) (w : F) : (L.toLinearMap₂ v) w = (L v) w

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] [UniformAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsUniformEmbedding (ContinuousLinearMap.restrictScalars 𝕜')

@[deprecated ContinuousLinearMap.isUniformEmbedding_restrictScalars]

theorem ContinuousLinearMap.uniformEmbedding_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] [UniformAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsUniformEmbedding (ContinuousLinearMap.restrictScalars 𝕜')

Alias of ContinuousLinearMap.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] [UniformAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : UniformContinuous (ContinuousLinearMap.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] [TopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsEmbedding (ContinuousLinearMap.restrictScalars 𝕜')

@[deprecated ContinuousLinearMap.isEmbedding_restrictScalars]

theorem ContinuousLinearMap.embedding_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] [TopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsEmbedding (ContinuousLinearMap.restrictScalars 𝕜')

Alias of ContinuousLinearMap.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] [TopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type u_4) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Continuous (ContinuousLinearMap.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] [TopologicalAddGroup 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] [TopologicalAddGroup 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] : ↑(ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = ContinuousLinearMap.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] [TopologicalAddGroup 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] : ⇑(ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'

Continuous linear equivalences

@[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] [TopologicalAddGroup G] [TopologicalAddGroup 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_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] [TopologicalAddGroup G] [TopologicalAddGroup 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.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] [TopologicalAddGroup G] [TopologicalAddGroup 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.

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] [TopologicalAddGroup G] [TopologicalAddGroup 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] [TopologicalAddGroup G] [TopologicalAddGroup 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] [TopologicalAddGroup G] [TopologicalAddGroup 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] [TopologicalAddGroup G] [TopologicalAddGroup 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] [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm