feat: if E is finite dimensional, E →L[𝕜] F has the product topology

Mathlib.lean

@@ -7346,6 +7346,7 @@ public import Mathlib.Topology.Algebra.Module.Simple
 public import Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
 public import Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
+public import Mathlib.Topology.Algebra.Module.Spaces.FiniteDimensionCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -409,14 +409,21 @@ theorem TotallyBounded.isVonNBounded {s : Set E} (hs : TotallyBounded s) :
     have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
       h'' <| mk_mem_prod hz1 hz2
     refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
-    -- TODO: with dot notation, Lean timeouts on the next line. Why?
-    exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
+    exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self
   else
     haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
     exact Bornology.IsVonNBounded.of_boundedSpace
 
 end IsUniformAddGroup
 
+variable (𝕜) in
+theorem IsCompact.isVonNBounded [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E}
+    (hs : IsCompact s) : Bornology.IsVonNBounded 𝕜 s :=
+  letI := IsTopologicalAddGroup.rightUniformSpace E
+  haveI := isUniformAddGroup_of_addCommGroup (G := E)
+  hs.totallyBounded.isVonNBounded 𝕜
+
 variable (𝕜) in
 theorem Filter.Tendsto.isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
     [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]

Mathlib/Analysis/LocallyConvex/Montel.lean

@@ -78,7 +78,7 @@ end Normed
 variable {𝕜₁ 𝕜₂ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
 variable {E F : Type*}
   [AddCommGroup E] [Module 𝕜₁ E]
-  [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜₁ E]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E]
   [AddCommGroup F] [Module 𝕜₂ F]
   [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F]
 
@@ -110,7 +110,7 @@ def _root_.ContinuousLinearEquiv.toCompactConvergenceCLM [T1Space E] [MontelSpac
     apply hs.mono
     apply UniformConvergenceCLM.topologicalSpace_mono
     intro x hx
-    exact hx.totallyBounded.isVonNBounded 𝕜₁
+    exact hx.isVonNBounded 𝕜₁
   continuous_invFun := by
     apply continuous_of_continuousAt_zero (LinearEquiv.toCompactConvergenceCLM σ E F).symm
     rw [ContinuousAt, _root_.map_zero, CompactConvergenceCLM.hasBasis_nhds_zero.tendsto_iff

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -536,35 +536,6 @@ def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
       rw [norm_smul, mul_comm]
       gcongr <;> apply norm_le_pi_norm }
 
-/-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications
-are. -/
-theorem continuousWithinAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {s : Set X} {x : X} :
-    ContinuousWithinAt f s x ↔ ∀ y, ContinuousWithinAt (fun q ↦ f q y) s x := by
-  refine ⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun h ↦ ?_⟩
-  let e : (E →L[𝕜] F) ≃L[𝕜] Fin (finrank 𝕜 E) → F :=
-    ((ContinuousLinearEquiv.ofFinrankEq (finrank_fin_fun 𝕜).symm).arrowCongr
-      (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing _)
-  rw [e.toHomeomorph.isInducing.continuousWithinAt_iff]
-  exact continuousWithinAt_pi.mpr fun i ↦ h _
-
-/-- A family of continuous linear maps is continuous on `s` iff all its applications are. -/
-theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {s : Set X} :
-    ContinuousOn f s ↔ ∀ y, ContinuousOn (fun x ↦ f x y) s := by
-  simp_rw [ContinuousOn, continuousWithinAt_clm_apply, imp_forall_iff]
-  exact forall_comm
-
-/-- A family of continuous linear maps is continuous at a point iff all its applications are. -/
-theorem continuousAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {x : X} :
-    ContinuousAt f x ↔ ∀ y, ContinuousAt (fun q ↦ f q y) x := by
-  simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_apply]
-
-theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} : Continuous f ↔ ∀ y, Continuous (f · y) := by
-  simp_rw [← continuousOn_univ, continuousOn_clm_apply]
-
 end CompleteField
 
 section LocallyCompactField

Mathlib/Analysis/Normed/Operator/Compact.lean

@@ -355,18 +355,16 @@ variable {𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁] [Nontrivial
 @[continuity]
 theorem IsCompactOperator.continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
     Continuous f := by
-  letI : UniformSpace M₂ := IsTopologicalAddGroup.rightUniformSpace _
-  haveI : IsUniformAddGroup M₂ := isUniformAddGroup_of_addCommGroup
   -- Since `f` is linear, we only need to show that it is continuous at zero.
   -- Let `U` be a neighborhood of `0` in `M₂`.
   refine continuous_of_continuousAt_zero f fun U hU => ?_
   rw [map_zero] at hU
   -- The compactness of `f` gives us a compact set `K : Set M₂` such that `f ⁻¹' K` is a
   -- neighborhood of `0` in `M₁`.
   rcases hf with ⟨K, hK, hKf⟩
-  -- But any compact set is totally bounded, hence Von-Neumann bounded. Thus, `K` absorbs `U`.
+  -- But any compact set Von-Neumann bounded. Thus, `K` absorbs `U`.
   -- This gives `r > 0` such that `∀ a : 𝕜₂, r ≤ ‖a‖ → K ⊆ a • U`.
-  rcases (hK.totallyBounded.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩
+  rcases (hK.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩
   -- Choose `c : 𝕜₂` with `r < ‖c‖`.
   rcases NormedField.exists_lt_norm 𝕜₁ r with ⟨c, hc⟩
   have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm

Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean

@@ -65,11 +65,11 @@ notation:25 E " →L_c[" R "] " F => CompactConvergenceCLM (RingHom.id R) E F
 namespace CompactConvergenceCLM
 
 instance continuousSMul [RingHomSurjective σ] [RingHomIsometric σ]
-    [UniformSpace E] [IsUniformAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F]
+    [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F]
     [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] :
     ContinuousSMul 𝕜₂ (E →SL_c[σ] F) :=
   UniformConvergenceCLM.continuousSMul σ F { S | IsCompact S }
-    (fun _ hs => hs.totallyBounded.isVonNBounded 𝕜₁)
+    (fun _ hs => hs.isVonNBounded 𝕜₁)
 
 instance instContinuousEvalConst [TopologicalSpace E] [TopologicalSpace F]
     [IsTopologicalAddGroup F] : ContinuousEvalConst (E →SL_c[σ] F) E F :=

Mathlib/Topology/Algebra/Module/Spaces/FiniteDimensionCLM.lean

@@ -0,0 +1,234 @@
+/-
+Copyright (c) 2026 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+module
+
+public import Mathlib.Topology.Algebra.Module.FiniteDimension
+public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
+public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
+public import Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
+
+/-!
+# Topology on `E →L[𝕜] F` when `E` is finite dimensional
+
+When `E` is a finite dimensional T2 vector space over a complete nontrivially normed field,
+then the topology of bounded convergence on `E →L[𝕜] F` coincides with the toplogy of
+pointwise convergence.
+
+In fact, the same applies to `E →L_c[𝕜] F` (with the topology of compact convergence) and,
+more generally, to `E →Lᵤ[𝕜, 𝔖] F` for any covering family `𝔖 : Set (Set E)` of bounded subsets
+of `E`.
+
+## TODO
+
+- Write `ContinuousLinearEquiv.piRing` in this setting.
+
+-/
+
+@[expose] public section
+
+open Module ContinuousLinearMap LinearMap Topology Bornology
+
+namespace UniformConvergenceCLM
+
+variable {ι 𝕜 R E F V Vᵤ : Type*} [Semiring R] [NontriviallyNormedField 𝕜]
+  [AddCommGroup E] [AddCommGroup F] [AddCommGroup V] [AddCommGroup Vᵤ]
+  [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 V] [Module 𝕜 Vᵤ]
+  [Module R V] [SMulCommClass 𝕜 R V]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F]
+  [TopologicalSpace V] [IsTopologicalAddGroup V] [UniformSpace Vᵤ] [IsUniformAddGroup Vᵤ]
+  [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 V] [ContinuousSMul 𝕜 Vᵤ]
+  [ContinuousConstSMul R V]
+  [CompleteSpace 𝕜] [T2Space E] -- hypotheses for automatic continuity in finite dimension
+  {𝔖 : Set (Set E)} {𝔗 : Set (Set F)}
+
+open Basis in
+theorem continuous_constrL [Finite ι] (b : Basis ι 𝕜 E)
+    (h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜 s) :
+    Continuous (Y := E →Lᵤ[𝕜, 𝔖] V) b.constrL := by
+  rcases nonempty_fintype ι
+  letI Φ : (ι → V) →ₗ[𝕜] (E →L[𝕜] V) := ⟨⟨b.constrL, by simp [constrL]⟩, by simp [constrL]⟩
+  -- This gets a bit painful because of the type alias
+  suffices Continuous fun (p : _ × _) ↦ Φ p.1 p.2 from
+    UniformConvergenceCLM.continuous_of_continuous_uncurry h𝔖 Φ this
+  simp only [Φ, LinearMap.coe_mk, AddHom.coe_mk, b.constrL_apply, equivFun_apply, ← equivFunL_apply]
+  fun_prop
+
+variable (R) in
+/-- `Basis.constrL` upgraded to a `ContinuousLinearEquiv`, between `ι → V`
+and `E →Lᵤ[𝕜, 𝔖] V`. -/
+protected noncomputable def constrCLE [Finite ι] (b : Basis ι 𝕜 E)
+    (h𝔖₁ : ∀ s ∈ 𝔖, IsVonNBounded 𝕜 s)
+    (h𝔖₂ : ⋃₀ 𝔖 = .univ) :
+    (ι → V) ≃L[R] (E →Lᵤ[𝕜, 𝔖] V) :=
+  have := UniformConvergenceCLM.continuousEvalConst (.id 𝕜) V _ h𝔖₂
+  { toFun := b.constrL
+    invFun f i := f (b i)
+    map_add' f g := toLinearMap_injective (map_add (b.constr R) f g)
+    map_smul' c f := toLinearMap_injective (map_smul (b.constr R) c f)
+    left_inv := b.constr R |>.left_inv
+    right_inv _ := toLinearMap_injective (b.constr R |>.right_inv _)
+    continuous_toFun := UniformConvergenceCLM.continuous_constrL b h𝔖₁
+    continuous_invFun := continuous_pi fun i ↦ continuous_eval_const (b i) }
+
+/-- If `E` is finite dimensional, the topology of `𝔖`-convergence on `E →Lᵤ[𝕜, 𝔖] F`
+identifies with the product topology. -/
+theorem isEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E]
+    (h𝔖₁ : ∀ s ∈ 𝔖, IsVonNBounded 𝕜 s)
+    (h𝔖₂ : ⋃₀ 𝔖 = .univ) :
+    IsEmbedding ((↑) : (E →Lᵤ[𝕜, 𝔖] V) → (E → V)) := by
+  have := UniformConvergenceCLM.continuousEvalConst (.id 𝕜) V _ h𝔖₂
+  let b : Basis _ 𝕜 E := Free.chooseBasis 𝕜 E
+  have : Continuous (fun (f : E → V) i ↦ f (b i)) := continuous_pi fun i ↦ continuous_apply _
+  exact .of_comp continuous_coeFun this
+    (UniformConvergenceCLM.constrCLE 𝕜 b h𝔖₁ h𝔖₂).symm.toHomeomorph.isEmbedding
+
+theorem isUniformEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E]
+    (h𝔖₁ : ∀ s ∈ 𝔖, IsVonNBounded 𝕜 s)
+    (h𝔖₂ : ⋃₀ 𝔖 = .univ) :
+    IsUniformEmbedding ((↑) : (E →Lᵤ[𝕜, 𝔖] Vᵤ) → (E → Vᵤ)) :=
+  let Φ : (E →Lᵤ[𝕜, 𝔖] Vᵤ) →ₗ[𝕜] (E → Vᵤ) := LinearMap.ltoFun _ _ _ _ ∘ₗ coeLM _
+  AddMonoidHom.isUniformEmbedding_of_isEmbedding (f := Φ)
+    (isEmbedding_coeFn_of_finiteDimensional h𝔖₁ h𝔖₂)
+
+end UniformConvergenceCLM
+
+section ContinuousLinearMap
+
+variable {ι 𝕜 R E F V Vᵤ : Type*} [Semiring R] [NontriviallyNormedField 𝕜]
+  [AddCommGroup E] [AddCommGroup F] [AddCommGroup V] [AddCommGroup Vᵤ]
+  [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 V] [Module 𝕜 Vᵤ]
+  [Module R V] [SMulCommClass 𝕜 R V]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F]
+  [TopologicalSpace V] [IsTopologicalAddGroup V] [UniformSpace Vᵤ] [IsUniformAddGroup Vᵤ]
+  [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 V] [ContinuousSMul 𝕜 Vᵤ]
+  [ContinuousConstSMul R V]
+  [CompleteSpace 𝕜] [T2Space E] -- hypotheses for automatic continuity in finite dimension
+
+theorem Module.Basis.continuous_constrL [Finite ι] (b : Basis ι 𝕜 E) :
+    Continuous (b.constrL : (ι → V) → (E →L[𝕜] V)) :=
+  UniformConvergenceCLM.continuous_constrL b (fun _ ↦ id)
+
+variable (R) in
+/-- `Basis.constrL` upgraded to a `ContinuousLinearEquiv`, between `ι → V`
+and `E →L[𝕜, 𝔖] V`. -/
+@[simps! apply symm_apply]
+protected noncomputable def Module.Basis.constrCLE [Finite ι] (b : Basis ι 𝕜 E) :
+    (ι → V) ≃L[R] (E →L[𝕜] V) :=
+  UniformConvergenceCLM.constrCLE R b (fun _ ↦ id) sUnion_isVonNBounded_eq_univ
+
+/-- If `E` is finite dimensional, the topology of bounded convergence on `E →L[𝕜] F`
+identifies with the product topology. -/
+theorem ContinuousLinearMap.isEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E] :
+    IsEmbedding ((↑) : (E →L[𝕜] V) → (E → V)) :=
+  UniformConvergenceCLM.isEmbedding_coeFn_of_finiteDimensional (fun _ ↦ id)
+    sUnion_isVonNBounded_eq_univ
+
+theorem ContinuousLinearMap.isUniformEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E] :
+    IsUniformEmbedding ((↑) : (E →L[𝕜] Vᵤ) → (E → Vᵤ)) :=
+  UniformConvergenceCLM.isUniformEmbedding_coeFn_of_finiteDimensional (fun _ ↦ id)
+    sUnion_isVonNBounded_eq_univ
+
+/-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications
+are. -/
+theorem continuousWithinAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
+    {f : X → E →L[𝕜] V} {s : Set X} {x : X} :
+    ContinuousWithinAt f s x ↔ ∀ y, ContinuousWithinAt (fun q ↦ f q y) s x := by
+  simp [ContinuousLinearMap.isEmbedding_coeFn_of_finiteDimensional.continuousWithinAt_iff,
+    continuousWithinAt_pi]
+
+/-- A family of continuous linear maps is continuous on `s` iff all its applications are. -/
+theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
+    {f : X → E →L[𝕜] V} {s : Set X} :
+    ContinuousOn f s ↔ ∀ y, ContinuousOn (fun x ↦ f x y) s := by
+  simp [ContinuousLinearMap.isEmbedding_coeFn_of_finiteDimensional.continuousOn_iff,
+    continuousOn_pi]
+
+/-- A family of continuous linear maps is continuous at a point iff all its applications are. -/
+theorem continuousAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
+    {f : X → E →L[𝕜] V} {x : X} :
+    ContinuousAt f x ↔ ∀ y, ContinuousAt (fun q ↦ f q y) x := by
+  simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_apply]
+
+theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
+    {f : X → E →L[𝕜] V} : Continuous f ↔ ∀ y, Continuous (f · y) := by
+  simp_rw [← continuousOn_univ, continuousOn_clm_apply]
+
+end ContinuousLinearMap
+
+namespace PointwiseConvergenceCLM
+
+open scoped PointwiseConvergenceCLM
+open Set
+
+variable {ι 𝕜 R E F V Vᵤ : Type*} [Semiring R] [NontriviallyNormedField 𝕜]
+  [AddCommGroup E] [AddCommGroup F] [AddCommGroup V] [AddCommGroup Vᵤ]
+  [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 V] [Module 𝕜 Vᵤ]
+  [Module R V] [SMulCommClass 𝕜 R V]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F]
+  [TopologicalSpace V] [IsTopologicalAddGroup V] [UniformSpace Vᵤ] [IsUniformAddGroup Vᵤ]
+  [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 V] [ContinuousSMul 𝕜 Vᵤ]
+  [ContinuousConstSMul R V]
+  [CompleteSpace 𝕜] [T2Space E] -- hypotheses for automatic continuity in finite dimension
+
+theorem continuous_constrL [Finite ι] (b : Basis ι 𝕜 E) :
+    Continuous (Y := E →Lₚₜ[𝕜] V) b.constrL :=
+  UniformConvergenceCLM.continuous_constrL b (fun _ ↦ Finite.isVonNBounded)
+
+variable (R) in
+/-- `Basis.constrL` upgraded to a `ContinuousLinearEquiv`, between `ι → V`
+and `E →Lₚₜ[𝕜, 𝔖] V`. -/
+protected noncomputable def constrCLE [Finite ι] (b : Basis ι 𝕜 E) :
+    (ι → V) ≃L[R] (E →Lₚₜ[𝕜] V) :=
+  UniformConvergenceCLM.constrCLE R b (fun _ ↦ Finite.isVonNBounded) sUnion_finite_eq_univ
+
+end PointwiseConvergenceCLM
+
+namespace CompactConvergenceCLM
+
+open scoped CompactConvergenceCLM
+open Set
+
+variable {ι 𝕜 R E F V Vᵤ : Type*} [Semiring R] [NontriviallyNormedField 𝕜]
+  [AddCommGroup E] [AddCommGroup F] [AddCommGroup V] [AddCommGroup Vᵤ]
+  [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 V] [Module 𝕜 Vᵤ]
+  [Module R V] [SMulCommClass 𝕜 R V]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F]
+  [TopologicalSpace V] [IsTopologicalAddGroup V] [UniformSpace Vᵤ] [IsUniformAddGroup Vᵤ]
+  [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 V] [ContinuousSMul 𝕜 Vᵤ]
+  [ContinuousConstSMul R V]
+  [CompleteSpace 𝕜] [T2Space E] -- hypotheses for automatic continuity in finite dimension
+
+theorem continuous_constrL [Finite ι] (b : Basis ι 𝕜 E) :
+    Continuous (Y := E →L_c[𝕜] V) b.constrL :=
+  UniformConvergenceCLM.continuous_constrL b
+    (fun _ hS ↦ hS.isVonNBounded 𝕜)
+
+variable (R) in
+/-- `Basis.constrL` upgraded to a `ContinuousLinearEquiv`, between `ι → V`
+and `E →L_c[𝕜] V`. -/
+protected noncomputable def constrCLE [Finite ι] (b : Basis ι 𝕜 E) :
+    (ι → V) ≃L[R] (E →L_c[𝕜] V) :=
+  UniformConvergenceCLM.constrCLE R b (fun _ hS ↦ hS.isVonNBounded 𝕜) sUnion_isCompact_eq_univ
+
+/-- If `E` is finite dimensional, the topology of compact convergence on `E →L_c[𝕜] F`
+identifies with the product topology. -/
+theorem isEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E] :
+    IsEmbedding ((↑) : (E →L_c[𝕜] V) → (E → V)) :=
+  UniformConvergenceCLM.isEmbedding_coeFn_of_finiteDimensional (fun _ hS ↦ hS.isVonNBounded 𝕜)
+    sUnion_isCompact_eq_univ
+
+theorem isUniformEmbedding_coeFn_of_finiteDimensional
+    [FiniteDimensional 𝕜 E] :
+    IsUniformEmbedding ((↑) : (E →L_c[𝕜] Vᵤ) → (E → Vᵤ)) :=
+  UniformConvergenceCLM.isUniformEmbedding_coeFn_of_finiteDimensional
+    (fun _ hS ↦ hS.isVonNBounded 𝕜) sUnion_isCompact_eq_univ
+
+end CompactConvergenceCLM