feat(ContinuousMultilinearMap): generalize some definitions (leanprover-community#34491)

... from normes spaces to topological vector spaces

Author: urkud

Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

@@ -929,50 +929,6 @@ theorem norm_compContinuousMultilinearMap_le (g : G →L[𝕜] G') (f : Continuo
       ‖g (f m)‖ ≤ ‖g‖ * (‖f‖ * ∏ i, ‖m i‖) := g.le_opNorm_of_le <| f.le_opNorm _
       _ = _ := (mul_assoc _ _ _).symm
 
-variable (𝕜 E G G')
-
-/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous bilinear map. -/
-def compContinuousMultilinearMapL :
-    (G →L[𝕜] G') →L[𝕜] ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E G' :=
-  LinearMap.mkContinuous₂
-    (LinearMap.mk₂ 𝕜 compContinuousMultilinearMap (fun _ _ _ => rfl) (fun _ _ _ => rfl)
-      (fun f g₁ g₂ => by ext1; apply f.map_add)
-      (fun c f g => by ext1; simp))
-    1
-    fun f g => by rw [one_mul]; exact f.norm_compContinuousMultilinearMap_le g
-
-variable {𝕜 G G'}
-
-/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled
-continuous linear equiv. -/
-def _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrRight (g : G ≃L[𝕜] G') :
-    ContinuousMultilinearMap 𝕜 E G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G' :=
-  { compContinuousMultilinearMapL 𝕜 E G G' g.toContinuousLinearMap with
-    invFun := compContinuousMultilinearMapL 𝕜 E G' G g.symm.toContinuousLinearMap
-    left_inv := by
-      intro f
-      ext1 m
-      simp [compContinuousMultilinearMapL]
-    right_inv := by
-      intro f
-      ext1 m
-      simp [compContinuousMultilinearMapL]
-    continuous_invFun :=
-      (compContinuousMultilinearMapL 𝕜 E G' G g.symm.toContinuousLinearMap).continuous }
-
-@[simp]
-theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm (g : G ≃L[𝕜] G') :
-    (g.continuousMultilinearMapCongrRight E).symm = g.symm.continuousMultilinearMapCongrRight E :=
-  rfl
-
-variable {E}
-
-@[simp]
-theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply (g : G ≃L[𝕜] G')
-    (f : ContinuousMultilinearMap 𝕜 E G) :
-    g.continuousMultilinearMapCongrRight E f = (g : G →L[𝕜] G').compContinuousMultilinearMap f :=
-  rfl
-
 /-- Flip arguments in `f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'` to get
 `ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')` -/
 @[simps! apply_apply]
@@ -1099,31 +1055,12 @@ theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 
     (f i : E i →L[𝕜] E₁ i)).norm_compContinuous_linearIsometry_le
       fun i => (f i).symm.toLinearIsometry
 
-/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
-This implementation fixes `f : Π i, E i →L[𝕜] E₁ i`.
-
-Actually, the map is multilinear in `f`,
-see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.
-
-For a version fixing `g` and varying `f`, see `compContinuousLinearMapLRight`. -/
-def compContinuousLinearMapL (f : ∀ i, E i →L[𝕜] E₁ i) :
-    ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
-  LinearMap.mkContinuous
-    { toFun := fun g => g.compContinuousLinearMap f
-      map_add' := fun _ _ => rfl
-      map_smul' := fun _ _ => rfl }
-    (∏ i, ‖f i‖)
-    fun _ => (norm_compContinuousLinearMap_le _ _).trans_eq (mul_comm _ _)
-
-@[simp]
-theorem compContinuousLinearMapL_apply (g : ContinuousMultilinearMap 𝕜 E₁ G)
-    (f : ∀ i, E i →L[𝕜] E₁ i) : compContinuousLinearMapL f g = g.compContinuousLinearMap f :=
-  rfl
 
 variable (G) in
 theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
-    ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
-  LinearMap.mkContinuous_norm_le _ (by positivity) _
+    ‖compContinuousLinearMapL (F := G) f‖ ≤ ∏ i, ‖f i‖ :=
+  ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun g ↦
+    norm_compContinuousLinearMap_le _ _ |>.trans_eq <| mul_comm _ _
 
 /-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
 This implementation fixes `g : ContinuousMultilinearMap 𝕜 E₁ G`.
@@ -1215,46 +1152,6 @@ lemma fderivCompContinuousLinearMap_apply [DecidableEq ι]
     f.fderivCompContinuousLinearMap g dg v = ∑ i, f fun j ↦ (update g i (dg i) j) (v j) := by
   simp [fderivCompContinuousLinearMap]
 
-variable (G)
-
-/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear equiv,
-given `f : Π i, E i ≃L[𝕜] E₁ i`. -/
-def _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft (f : ∀ i, E i ≃L[𝕜] E₁ i) :
-    ContinuousMultilinearMap 𝕜 E₁ G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
-  { compContinuousLinearMapL fun i => (f i : E i →L[𝕜] E₁ i) with
-    invFun := compContinuousLinearMapL fun i => ((f i).symm : E₁ i →L[𝕜] E i)
-    continuous_toFun := (compContinuousLinearMapL fun i => (f i : E i →L[𝕜] E₁ i)).continuous
-    continuous_invFun :=
-      (compContinuousLinearMapL fun i => ((f i).symm : E₁ i →L[𝕜] E i)).continuous
-    left_inv := by
-      intro g
-      ext1 m
-      simp only [LinearMap.toFun_eq_coe, ContinuousLinearMap.coe_coe,
-        compContinuousLinearMapL_apply, compContinuousLinearMap_apply,
-        ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.apply_symm_apply]
-    right_inv := by
-      intro g
-      ext1 m
-      simp only [compContinuousLinearMapL_apply, LinearMap.toFun_eq_coe,
-        ContinuousLinearMap.coe_coe, compContinuousLinearMap_apply, ContinuousLinearEquiv.coe_coe,
-        ContinuousLinearEquiv.symm_apply_apply] }
-
-@[simp]
-theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm
-    (f : ∀ i, E i ≃L[𝕜] E₁ i) :
-    (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f).symm =
-      .continuousMultilinearMapCongrLeft G fun i : ι => (f i).symm :=
-  rfl
-
-variable {G}
-
-@[simp]
-theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply
-    (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i ≃L[𝕜] E₁ i) :
-    ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f g =
-      g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i) :=
-  rfl
-
 /-- One of the components of the iterated derivative of a continuous multilinear map. Given a
 bijection `e` between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a
 continuous multilinear map of `k` vectors `v₁, ..., vₖ`, mapping them

Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

@@ -336,7 +336,7 @@ continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operati
 theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear (g : G →L[𝕜] E) :
     IsBoundedLinearMap 𝕜 fun f : ContinuousMultilinearMap 𝕜 (fun _ : ι => E) F =>
       f.compContinuousLinearMap fun _ => g :=
-  (ContinuousMultilinearMap.compContinuousLinearMapL (ι := ι) (G := F) (fun _ ↦ g))
+  (ContinuousMultilinearMap.compContinuousLinearMapL (ι := ι) (F := F) (fun _ ↦ g))
     |>.isBoundedLinearMap
 
 end

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -790,6 +790,29 @@ theorem mem_closure_iff_nhds_one {x : G} {s : Set G} :
   rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
   simp_rw [Set.mem_setOf, id]
 
+/-- A monoid homomorphism (a bundled morphism of a type that implements `MonoidHomClass`)
+from a topological group to a topological monoid is continuous
+provided that it is continuous at one.
+
+This version assumes that `f x → 1` as `x → 1`,
+saving a rewrite of `f 1 = 1` compared to `continuous_of_continuousAt_one` in some cases.
+See also `uniformContinuous_of_continuousAt_one`. -/
+@[to_additive
+  /-- An additive monoid homomorphism (a bundled morphism of a type that implements
+  `AddMonoidHomClass`) from an additive topological group to an additive topological monoid is
+  continuous provided that it is continuous at zero.
+
+  This version assumes that `f x → 0` as `x → 0`,
+  saving a rewrite of `f 0 = 0` compared to `continuous_of_continuousAt_zero` in some cases.
+  See also `uniformContinuous_of_continuousAt_zero`. -/]
+theorem continuous_of_tendsto_nhds_one {M hom : Type*} [MulOneClass M] [TopologicalSpace M]
+    [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom)
+    (hf : Tendsto f (𝓝 1) (𝓝 1)) :
+    Continuous f :=
+  continuous_iff_continuousAt.2 fun x ↦ by
+    simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
+      map_mul, mul_one] using hf.const_mul (f x)
+
 /-- A monoid homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) from a
 topological group to a topological monoid is continuous provided that it is continuous at one. See
 also `uniformContinuous_of_continuousAt_one`. -/
@@ -802,9 +825,7 @@ theorem continuous_of_continuousAt_one {M hom : Type*} [MulOneClass M] [Topologi
     [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom)
     (hf : ContinuousAt f 1) :
     Continuous f :=
-  continuous_iff_continuousAt.2 fun x => by
-    simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
-      map_mul, map_one, mul_one] using hf.tendsto.const_mul (f x)
+  continuous_of_tendsto_nhds_one f <| by simpa using hf.tendsto
 
 @[to_additive continuous_of_continuousAt_zero₂]
 theorem continuous_of_continuousAt_one₂ {H M : Type*} [CommMonoid M] [TopologicalSpace M]

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

@@ -5,7 +5,9 @@ Authors: Yury Kudryashov
 -/
 module
 
+public import Mathlib.Topology.Algebra.Module.Equiv
 public import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
+public import Mathlib.Topology.Algebra.Module.StrongTopology
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
 public import Mathlib.Topology.Algebra.SeparationQuotient.Section
 public import Mathlib.Topology.Hom.ContinuousEvalConst
@@ -212,6 +214,53 @@ theorem hasBasis_nhds_zero :
       { f | MapsTo f SV.1 SV.2 } :=
   hasBasis_nhds_zero_of_basis (Filter.basis_sets _)
 
+theorem eventually_nhds_zero_mapsTo {s : Set (∀ i, E i)} (hs : IsVonNBounded 𝕜 s)
+    {U : Set F} (hu : U ∈ 𝓝 0) :
+    ∀ᶠ f : ContinuousMultilinearMap 𝕜 E F in 𝓝 0, MapsTo f s U :=
+  hasBasis_nhds_zero.mem_of_mem (i := (s, U)) ⟨hs, hu⟩
+
+theorem isVonNBounded_image2_apply [ContinuousConstSMul 𝕜 F]
+    {S : Set (ContinuousMultilinearMap 𝕜 E F)} (hS : IsVonNBounded 𝕜 S)
+    {s : Set (∀ i, E i)} (hs : IsVonNBounded 𝕜 s) :
+    IsVonNBounded 𝕜 (Set.image2 (fun f x ↦ f x) S s) := by
+  intro U hU
+  filter_upwards [hS (eventually_nhds_zero_mapsTo hs hU)] with c hc
+  rw [image2_subset_iff]
+  intro f hf x hx
+  rcases hc hf with ⟨g, hg, rfl⟩
+  exact smul_mem_smul_set (hg hx)
+
+section CompContinuousLinearMap
+variable {E₁ : ι → Type*} [∀ i, TopologicalSpace (E₁ i)] [ContinuousConstSMul 𝕜 F]
+  [∀ i, AddCommGroup (E₁ i)] [∀ i, Module 𝕜 (E₁ i)]
+
+/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
+Given a family of continuous linear maps `f : Π i, E i →L[𝕜] E₁ i`,
+this function returns a continuous linear maps between the spaces of continuous multilinear maps
+on `Π i, E₁ i` and on `Π i, E i`.
+The map sends `g` to the map given by `v ↦ g (fun i ↦ f i (v i))`.
+
+Actually, the map is multilinear in `f`,
+see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.
+
+For a version fixing `g` and varying `f`, see `compContinuousLinearMapLRight`. -/
+@[simps! apply]
+def compContinuousLinearMapL (f : ∀ i, E i →L[𝕜] E₁ i) :
+    ContinuousMultilinearMap 𝕜 E₁ F →L[𝕜] ContinuousMultilinearMap 𝕜 E F :=
+  letI aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
+    { toFun g := g.compContinuousLinearMap f
+      map_add' _ _ := by ext; simp
+      map_smul' _ _ := by ext; simp }
+  { toLinearMap := aux
+    cont := by
+      apply continuous_of_tendsto_nhds_zero aux
+      rw [hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero]
+      rintro ⟨U, V⟩ ⟨hU, hV⟩
+      set φ : (∀ i, E i) →L[𝕜] (∀ i, E₁ i) := .piMap f
+      exact ⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩ }
+
+end CompContinuousLinearMap
+
 variable [∀ i, ContinuousSMul 𝕜 (E i)]
 
 instance : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
@@ -280,3 +329,127 @@ theorem tsum_eval [T2Space F] {α : Type*} {p : α → ContinuousMultilinearMap
   (hasSum_eval hp.hasSum m).tsum_eq.symm
 
 end ContinuousMultilinearMap
+
+namespace ContinuousLinearMap
+
+variable {𝕜 ι : Type*} {E : ι → Type*} {F G : Type*} [NormedField 𝕜] [∀ i, TopologicalSpace (E i)]
+  [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+  [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+  [ContinuousConstSMul 𝕜 F]
+  [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G]
+  [ContinuousConstSMul 𝕜 G]
+
+variable (𝕜 E F G) in
+/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous bilinear map.
+
+Given a continuous linear map `f : F →L[𝕜] G`
+and a continuous multilinear map `g` from `Π i, E i` to `F`,
+this function returns `f ∘ g` as a continuous multilinear map.
+
+With this order of arguments, the function is continuous in `g` (for each fixed `f`)
+and is continuous in `f` (as a function to the space of continuous linear maps).
+Note that for general topological vector spaces, it is not guaranteed to be continuous in `(g, f)`.
+-/
+def compContinuousMultilinearMapL :
+    (F →L[𝕜] G) →L[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
+  letI aux : (F →L[𝕜] G) →ₗ[𝕜]
+      ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
+    { toFun g :=
+        letI aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
+          { toFun := g.compContinuousMultilinearMap
+            map_add' _ _ := by ext; simp
+            map_smul' _ _ := by ext; simp }
+        { toLinearMap := aux₁
+          cont := by
+            apply continuous_of_tendsto_nhds_zero aux₁
+            rw [ContinuousMultilinearMap.hasBasis_nhds_zero.tendsto_iff
+              ContinuousMultilinearMap.hasBasis_nhds_zero]
+            rintro ⟨U, V⟩ ⟨hU, hV⟩
+            refine ⟨(U, g ⁻¹' V), ⟨hU, ?_⟩, ?_⟩
+            · exact (map_continuous g).tendsto 0 <| by simpa
+            · exact fun f hf ↦ hf
+        }
+      map_add' _ _ := by ext; simp
+      map_smul' _ _ := by ext; simp }
+  { toLinearMap := aux
+    cont := by
+      apply continuous_of_tendsto_nhds_zero aux
+      rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff <|
+        ContinuousLinearMap.hasBasis_nhds_zero_of_basis <|
+        ContinuousMultilinearMap.hasBasis_nhds_zero]
+      rintro ⟨U, V, W⟩ ⟨hU, hV, hW⟩
+      refine ⟨(.image2 (fun f v ↦ f v) U V, W), ⟨?_, hW⟩, ?_⟩
+      · exact ContinuousMultilinearMap.isVonNBounded_image2_apply hU hV
+      · exact fun g hg f hf m hm ↦ hg _ <| mem_image2_of_mem hf hm }
+
+@[simp]
+theorem compContinuousMultilinearMapL_apply (g : F →L[𝕜] G) (f : ContinuousMultilinearMap 𝕜 E F) :
+    compContinuousMultilinearMapL 𝕜 E F G g f = g.compContinuousMultilinearMap f :=
+  rfl
+
+end ContinuousLinearMap
+
+namespace ContinuousLinearEquiv
+
+variable {𝕜 ι : Type*} {E E₁ : ι → Type*} {F G : Type*} [NormedField 𝕜]
+  [∀ i, TopologicalSpace (E i)] [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+  [∀ i, TopologicalSpace (E₁ i)] [∀ i, AddCommGroup (E₁ i)] [∀ i, Module 𝕜 (E₁ i)]
+  [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+  [ContinuousConstSMul 𝕜 F]
+  [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G]
+  [ContinuousConstSMul 𝕜 G]
+
+variable (F) in
+/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear equiv.
+Given a family of continuous linear equivalences `f : Π i, E i ≃L[𝕜] E₁ i`,
+this function returns a continuous linear equivalence
+between the space of continuous multilinear maps with domain `Π i, E i` and codomain `F`
+and the space of multilinear maps with domain `Π i, E₁ i` and the same codomain,
+by composing the multilinear maps with `f`. -/
+def continuousMultilinearMapCongrLeft (f : ∀ i, E i ≃L[𝕜] E₁ i) :
+    ContinuousMultilinearMap 𝕜 E₁ F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E F where
+  __ := ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i)
+  invFun := ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm
+  left_inv g := by ext; simp
+  right_inv g := by ext; simp
+
+@[simp]
+theorem continuousMultilinearMapCongrLeft_symm
+    (f : ∀ i, E i ≃L[𝕜] E₁ i) :
+    (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft F f).symm =
+      .continuousMultilinearMapCongrLeft F fun i : ι ↦ (f i).symm :=
+  rfl
+
+@[simp]
+theorem continuousMultilinearMapCongrLeft_apply
+    (g : ContinuousMultilinearMap 𝕜 E₁ F) (f : ∀ i, E i ≃L[𝕜] E₁ i) :
+    ContinuousLinearEquiv.continuousMultilinearMapCongrLeft F f g =
+      g.compContinuousLinearMap fun i ↦ (f i : E i →L[𝕜] E₁ i) :=
+  rfl
+
+variable (E) in
+/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous linear equiv.
+Given a continuous linear equivalence `g : F ≃L[𝕜] G`,
+this function builds a continuous linear equivalence
+between the space of continuous multilinear maps with codomain `F`
+and the space of continuous multilinear maps with codomain `G`,
+by composing these maps with `g` or `g.symm`. -/
+def continuousMultilinearMapCongrRight (g : F ≃L[𝕜] G) :
+    ContinuousMultilinearMap 𝕜 E F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G where
+  __ := ContinuousLinearMap.compContinuousMultilinearMapL _ _ _ _ g
+  invFun := ContinuousLinearMap.compContinuousMultilinearMapL _ _ _ _ g.symm
+  left_inv _ := by ext; simp
+  right_inv _ := by ext; simp
+
+@[simp]
+theorem continuousMultilinearMapCongrRight_symm (g : F ≃L[𝕜] G) :
+    (g.continuousMultilinearMapCongrRight E).symm = g.symm.continuousMultilinearMapCongrRight E :=
+  rfl
+
+@[simp]
+theorem continuousMultilinearMapCongrRight_apply (g : F ≃L[𝕜] G)
+    (f : ContinuousMultilinearMap 𝕜 E F) :
+    g.continuousMultilinearMapCongrRight E f = (g : F →L[𝕜] G).compContinuousMultilinearMap f :=
+  rfl
+
+end ContinuousLinearEquiv

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -831,9 +831,9 @@ variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Modul
 def toSpanSingletonCLE : E ≃L[𝕜] (𝕜 →L[𝕜] E) where
   toLinearEquiv := toSpanSingletonLE ..
   continuous_toFun := by
-    apply continuous_of_continuousAt_zero (toSpanSingletonLE _ _ _)
+    apply continuous_of_tendsto_nhds_zero (toSpanSingletonLE _ _ _)
     suffices ∀ s : Set 𝕜, IsVonNBounded 𝕜 s → ∀ U ∈ 𝓝 0, ∀ᶠ (a : E) in 𝓝 0, ∀ x ∈ s, x • a ∈ U by
-      simpa [ContinuousAt, ContinuousLinearMap.nhds_zero_eq, MapsTo]
+      simpa [ContinuousLinearMap.nhds_zero_eq, MapsTo]
     intro s hsb U hU
     rcases mem_nhds_prod_iff.mp <| continuous_smul.tendsto' (0 : 𝕜 × E) 0 (by simp) hU
       with ⟨V, hV, W, hW, hVW⟩