Topologies of uniform convergence on the space of continuous linear maps

In this file, we define the "topology of 𝔖-convergence" on E →L[𝕜] F, where 𝔖 : Set (Set E). It is the topology of uniform convergence on the elements of 𝔖. Similarly to UniformOnFun, we define a type synonym UniformConvergenceCLM for E →L[𝕜] F endowed with this topology.

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).

The most important examples for such topologies are:

• the topology of bounded convergence (also called the "strong topology" on the dual space), when 𝔖 is the set of IsVonNBounded subsets. This coincides with the operator norm topology in the case of NormedSpaces, and is declared as an instance on E →L[𝕜] F
• the topology of pointwise convergence (also called "weak-* topology" or "strong-operator topology" depending on the context), when 𝔖 is the set of finite sets or the set of singletons. This is declared as an instance on PointwiseConvergenceCLM.
• the topology of compact convergence, when 𝔖 is the set of compact sets. This is declared as an instance on CompactConvergenceCLM.

Main definitions

• UniformConvergenceCLM is a type synonym for E →SL[σ] F equipped with the 𝔖-topology. We denote it by E →SLᵤ[σ, 𝔖] F.
• UniformConvergenceCLM.instTopologicalSpace is the topology mentioned above for an arbitrary 𝔖.

Main statements

• UniformConvergenceCLM.instIsTopologicalAddGroup and UniformConvergenceCLM.instContinuousSMul show that the strong topology makes E →L[𝕜] F a topological vector space, with the assumptions on 𝔖 mentioned above.

Notation

• E →SLᵤ[σ, 𝔖] F is space of continuous linear maps equipped with the topology of 𝔖-convergence.

References

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

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 𝔖 (denoted E →SLᵤ[σ, 𝔖] 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)

def UniformConvergenceCLM.«term_→SLᵤ[_,_]_» : Lean.TrailingParserDescr

Given E and F two topological vector spaces and 𝔖 : Set (Set E), then UniformConvergenceCLM σ F 𝔖 (denoted E →SLᵤ[σ, 𝔖] 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

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

def UniformConvergenceCLM.«term_→Lᵤ[_,_]_» : Lean.TrailingParserDescr

Given E and F two topological vector spaces and 𝔖 : Set (Set E), then UniformConvergenceCLM σ F 𝔖 (denoted E →SLᵤ[σ, 𝔖] 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

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

@[implicit_reducible]

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 𝔖 = { coe := UniformConvergenceCLM.instFunLike._aux_1 σ F 𝔖, coe_injective' := ⋯ }

theorem UniformConvergenceCLM.ext {𝕜₁ : 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)} {f g : UniformConvergenceCLM σ F 𝔖} (h : ∀ (x : E), f x = g x) : f = g

theorem UniformConvergenceCLM.ext_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] [TopologicalSpace F] {𝔖 : Set (Set E)} {f g : UniformConvergenceCLM σ F 𝔖} : f = g ↔ ∀ (x : E), f x = g x

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

@[implicit_reducible]

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] [IsTopologicalAddGroup 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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

@[implicit_reducible]

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] [IsUniformAddGroup 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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : 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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : (instUniformSpace σ F 𝔖).toTopologicalSpace = 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] [IsUniformAddGroup 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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : Topology.IsEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)

@[implicit_reducible]

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] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : AddCommGroup (UniformConvergenceCLM σ F 𝔖)

Equations

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

@[simp]

theorem UniformConvergenceCLM.neg_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] [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (f : UniformConvergenceCLM σ F 𝔖) (x : E) : (-f) x = -f x

@[simp]

theorem UniformConvergenceCLM.add_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] [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (f g : UniformConvergenceCLM σ F 𝔖) (x : E) : (f + g) x = f x + g x

@[simp]

theorem UniformConvergenceCLM.sum_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] {ι : Type u_6} [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (t : Finset ι) (f : ι → UniformConvergenceCLM σ F 𝔖) (x : E) : (∑ d ∈ t, f d) x = ∑ d ∈ t, (f d) x

@[simp]

theorem UniformConvergenceCLM.sub_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] [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (f g : UniformConvergenceCLM σ F 𝔖) (x : E) : (f - g) x = f x - g x

@[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] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : ⇑0 = 0

instance UniformConvergenceCLM.instIsUniformAddGroup {𝕜₁ : 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] [IsUniformAddGroup F] (𝔖 : Set (Set E)) : IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖)

instance UniformConvergenceCLM.instIsTopologicalAddGroup {𝕜₁ : 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] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)

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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup F] [T2Space F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) : T2Space (UniformConvergenceCLM σ F 𝔖)

@[implicit_reducible]

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_6) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : DistribMulAction M (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instDistribMulAction σ F M 𝔖 = { smul := UniformConvergenceCLM.instDistribMulAction._aux_1 σ F M 𝔖, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem UniformConvergenceCLM.smul_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] {M : Type u_6} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) (c : M) (f : UniformConvergenceCLM σ F 𝔖) (x : E) : (c • f) x = c • f x

@[implicit_reducible]

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_6) [Semiring R] [Module R F] [SMulCommClass 𝕜₂ R F] [TopologicalSpace F] [ContinuousConstSMul R F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) : Module R (UniformConvergenceCLM σ F 𝔖)

Equations

• UniformConvergenceCLM.instModule σ F R 𝔖 = { toDistribMulAction := UniformConvergenceCLM.instDistribMulAction σ F R 𝔖, add_smul := ⋯, zero_smul := ⋯ }

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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup F] {ι : Type u_6} (𝔖 : 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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) {ι : Type u_6} {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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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_6} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [DistribMulAction 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_6} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup 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_6) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [IsUniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) : UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

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_6) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

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_6} {p : Filter ι} [UniformSpace F] [IsUniformAddGroup 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} {G : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] {𝕜₃ : Type u_6} [NormedField 𝕜₃] [Module 𝕜₃ G] {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [IsUniformAddGroup F] (g : F →SL[τ] G) (hg : IsUniformInducing ⇑g) (𝔖 : Set (Set E)) : IsUniformInducing g.comp

theorem UniformConvergenceCLM.isUniformEmbedding_postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} {F : Type u_4} {G : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] {𝕜₃ : Type u_6} [NormedField 𝕜₃] [Module 𝕜₃ G] {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [IsUniformAddGroup F] (g : F →SL[τ] G) (hg : IsUniformEmbedding ⇑g) (𝔖 : Set (Set E)) : IsUniformEmbedding 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] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] {𝔖 : Set (Set E)} (h𝔖 : Topology.IsCoherentWith 𝔖) (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)} [UniformSpace F] [IsUniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) : instUniformSpace σ F 𝔖₁ ≤ 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)} [TopologicalSpace F] [IsTopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) : instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

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

Let 𝔖 be a family of bounded subsets of F, and B : E × F → G a bilinear map. If B is (jointly) continuous, then it is 𝔖-hypocontinuous: in curried form, it defines a continuous linear map E →L[𝕜] (F →Lᵤ[𝕜, 𝔖] G).

Note that, in full generality, the converse is not true. See also ContinuousLinearMap.continuous_of_continuous_uncurry.

def ContinuousLinearMap.toUniformConvergenceCLM {𝕜₁ : 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] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (𝔖 : Set (Set E)) : (E →SL[σ] F) ≃ₗ[𝕜₂] UniformConvergenceCLM σ F 𝔖

The linear equivalence that maps a continuous linear map to the type copy endowed with the uniform convergence topology.

Equations

• ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖 = LinearEquiv.refl 𝕜₂ (E →SL[σ] F)

@[simp]

theorem ContinuousLinearMap.toUniformConvergenceCLM_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] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {𝔖 : Set (Set E)} {A : E →SL[σ] F} {x : E} : ((toUniformConvergenceCLM σ F 𝔖) A) x = A x

@[simp]

theorem ContinuousLinearMap.toUniformConvergenceCLM_symm_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] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {𝔖 : Set (Set E)} {A : UniformConvergenceCLM σ F 𝔖} {x : E} : ((toUniformConvergenceCLM σ F 𝔖).symm A) x = A x

def ContinuousLinearMap.precompUniformConvergenceCLM {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} (G : Type u_11) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (hL : Set.MapsTo (fun (x : Set E) => ⇑L '' x) 𝔖 𝔗) : UniformConvergenceCLM τ G 𝔗 →L[𝕜₃] UniformConvergenceCLM ρ G 𝔖

Pre-composition by a fixed continuous linear map as a continuous linear map for the uniform convergence topology.

Equations

• ContinuousLinearMap.precompUniformConvergenceCLM G 𝔖 𝔗 L hL = { toFun := fun (f : UniformConvergenceCLM τ G 𝔗) => ContinuousLinearMap.comp f L, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.precompUniformConvergenceCLM_apply {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} (G : Type u_11) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (hL : Set.MapsTo (fun (x : Set E) => ⇑L '' x) 𝔖 𝔗) (f : UniformConvergenceCLM τ G 𝔗) : (precompUniformConvergenceCLM G 𝔖 𝔗 L hL) f = comp f L

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

def ContinuousLinearMap.precomp_uniformConvergenceCLM {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} (G : Type u_11) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (hL : Set.MapsTo (fun (x : Set E) => ⇑L '' x) 𝔖 𝔗) : UniformConvergenceCLM τ G 𝔗 →L[𝕜₃] UniformConvergenceCLM ρ G 𝔖

Alias of ContinuousLinearMap.precompUniformConvergenceCLM.

---

Pre-composition by a fixed continuous linear map as a continuous linear map for the uniform convergence topology.

Equations

• @ContinuousLinearMap.precomp_uniformConvergenceCLM = @ContinuousLinearMap.precompUniformConvergenceCLM

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

theorem ContinuousLinearMap.precomp_uniformConvergenceCLM_apply {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} (G : Type u_11) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (hL : Set.MapsTo (fun (x : Set E) => ⇑L '' x) 𝔖 𝔗) (f : UniformConvergenceCLM τ G 𝔗) : (precompUniformConvergenceCLM G 𝔖 𝔗 L hL) f = comp f L

Alias of ContinuousLinearMap.precompUniformConvergenceCLM_apply.

def ContinuousLinearMap.postcompUniformConvergenceCLM {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : UniformConvergenceCLM σ F 𝔖 →SL[τ] UniformConvergenceCLM ρ G 𝔖

Post-composition by a fixed continuous linear map as a continuous linear map for the uniform convergence topology.

Equations

• ContinuousLinearMap.postcompUniformConvergenceCLM 𝔖 L = { toFun := fun (f : UniformConvergenceCLM σ F 𝔖) => L.comp f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.postcompUniformConvergenceCLM_apply {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F 𝔖) : (postcompUniformConvergenceCLM 𝔖 L) f = L.comp f

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

def ContinuousLinearMap.postcomp_uniformConvergenceCLM {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : UniformConvergenceCLM σ F 𝔖 →SL[τ] UniformConvergenceCLM ρ G 𝔖

Alias of ContinuousLinearMap.postcompUniformConvergenceCLM.

---

Post-composition by a fixed continuous linear map as a continuous linear map for the uniform convergence topology.

Equations

• @ContinuousLinearMap.postcomp_uniformConvergenceCLM = @ContinuousLinearMap.postcompUniformConvergenceCLM

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

theorem ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (𝔖 : Set (Set E)) [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F 𝔖) : (postcompUniformConvergenceCLM 𝔖 L) f = L.comp f

Alias of ContinuousLinearMap.postcompUniformConvergenceCLM_apply.