Documentation

Mathlib.Topology.Algebra.Module.StrongTopology

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 #

Main statements #

References #

TODO #

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] [TopologicalAddGroup 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
Instances For
    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] [TopologicalAddGroup F] (𝔖 : Set (Set E)) :
    Equations
    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] [TopologicalAddGroup F] (𝔖 : Set (Set E)) :
    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)) :
    Equations
    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)) :
    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)) :

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

    Equations
    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)) :
    @[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.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.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)) :
    Embedding ((UniformOnFun.ofFun 𝔖) DFunLike.coe)
    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)) :
    Equations
    @[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)) :
    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)) :
    Equations
    • =
    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) :
    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)) :
    Equations
    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)) :
    Equations
    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) :
    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 | xSi.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 𝔖 | xSV.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𝔖, tnhds 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)) :
    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)) :
    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.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 : 𝔖₂ 𝔖₁) :
    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 : 𝔖₂ 𝔖₁) :

    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] :

    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
    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] :
    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] :
    Equations
    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] :
    Equations
    • =
    instance ContinuousLinearMap.instT2SpaceOfContinuousSMul {𝕜₁ : 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] :
    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 | xSi.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 | xSV.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] :
    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] :
    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), Unhds 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 𝕜₁ sBornology.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.

    @[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) :
    @[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) :
    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
    Instances For
      @[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) :
      @[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) :
      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
      Instances For
        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
        Instances For
          @[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
          @[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] :

          Alias of ContinuousLinearMap.isUniformEmbedding_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] :
          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] :
          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
          Instances For
            @[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] :

            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.
            Instances For
              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₂
              Instances For
                @[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