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

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]

def UniformConvergenceCLM.ofFun {𝕜₁ : 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)) : (E →SL[σ] F) ≃ UniformConvergenceCLM σ F 𝔖

Reinterpret f : E →SL[σ] F as an element of E →SLᵤ[σ, 𝔖] F.

Equations

• UniformConvergenceCLM.ofFun σ F 𝔖 = { toFun := fun (x : E →SL[σ] F) => x, invFun := fun (x : UniformConvergenceCLM σ F 𝔖) => x, left_inv := ⋯, right_inv := ⋯ }

@[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

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

@[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 : UniformConvergenceCLM σ 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.

Continuous linear equivalences

def UniformConvergenceCLM.piEquivL (𝕜 : Type u_6) [NormedField 𝕜] {E : Type u_7} {ι : Type u_8} (F : ι → Type u_9) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜 (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (𝔖 : Set (Set E)) : ((i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖) ≃L[𝕜] UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖

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

Equations

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

@[simp]

theorem UniformConvergenceCLM.piEquivL_apply (𝕜 : Type u_6) [NormedField 𝕜] {E : Type u_7} {ι : Type u_8} (F : ι → Type u_9) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜 (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (𝔖 : Set (Set E)) (T : (i : ι) → UniformConvergenceCLM (RingHom.id 𝕜) (F i) 𝔖) (e : E) (i : ι) : ((piEquivL 𝕜 F 𝔖) T) e i = (T i) e

@[simp]

theorem UniformConvergenceCLM.piEquivL_symm_apply (𝕜 : Type u_6) [NormedField 𝕜] {E : Type u_7} {ι : Type u_8} (F : ι → Type u_9) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜 (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (𝔖 : Set (Set E)) (T : UniformConvergenceCLM (RingHom.id 𝕜) ((i : ι) → F i) 𝔖) (e : E) (i : ι) : ((piEquivL 𝕜 F 𝔖).symm T i) e = T e i

def ContinuousLinearEquiv.uniformConvergenceCLMCongrSL {𝕜 : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} {𝕜₄ : Type u_9} {E : Type u_10} {F : Type u_11} {G : Type u_12} {H : Type u_13} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖) : UniformConvergenceCLM σ₁₄ H 𝔖 ≃SL[σ₄₃] UniformConvergenceCLM σ₂₃ G 𝔗

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

Equations

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

@[simp]

theorem ContinuousLinearEquiv.uniformConvergenceCLMCongrSL_apply {𝕜 : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} {𝕜₄ : Type u_9} {E : Type u_10} {F : Type u_11} {G : Type u_12} {H : Type u_13} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM σ₁₄ H 𝔖) (f : F) : ((e₁₂.uniformConvergenceCLMCongrSL e₄₃ 𝔖 𝔗 h) φ) f = e₄₃ (φ (e₁₂.symm f))

@[simp]

theorem ContinuousLinearEquiv.uniformConvergenceCLMCongrSL_symm_apply {𝕜 : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} {𝕜₄ : Type u_9} {E : Type u_10} {F : Type u_11} {G : Type u_12} {H : Type u_13} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM σ₂₃ G 𝔗) (e : E) : ((e₁₂.uniformConvergenceCLMCongrSL e₄₃ 𝔖 𝔗 h).symm φ) e = e₄₃.symm (φ (e₁₂ e))

def ContinuousLinearEquiv.uniformConvergenceCLMCongr {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} {H : Type u_10} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) : UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖 ≃L[𝕜] UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗

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

Equations

• e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h = e₁.uniformConvergenceCLMCongrSL e₂ 𝔖 𝔗 h

@[simp]

theorem ContinuousLinearEquiv.uniformConvergenceCLMCongr_apply {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} {H : Type u_10} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖) (f : F) : ((e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h) φ) f = e₂ (φ (e₁.symm f))

@[simp]

theorem ContinuousLinearEquiv.uniformConvergenceCLMCongr_symm_apply {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} {H : Type u_10} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗) (e : E) : ((e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h).symm φ) e = e₂.symm (φ (e₁ e))