feat(topology/algebra/module/basic): define continuous_(semi)linear_m…

…ap_class (#14674)

This PR brings the morphism refactor to continuous (semi)linear maps. We define `continuous_semilinear_map_class` and `continuous_linear_map_class` in a way that parallels the non-continuous versions, along with a few extras (i.e. `add_monoid_hom_class` instance for `normed_group_hom`).

A few things I was not too sure about:
- When generalizing lemmas to a morphism class rather than a particular type of morphism, I used `𝓕` as the type (instead of just `F` as is done for most `fun_like` types) to avoid clashing with our convention of using `E`, `F`, etc for e.g. vector spaces.
- Namespacing: I placed lemmas like `isometry_of_norm`, `continuous_of_bound`, etc, under the `add_monoid_hom_class` namespace. Maybe the root namespace would make sense here.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

src/analysis/calculus/deriv.lean

@@ -991,7 +991,7 @@ has_fderiv_at_filter.is_O_sub h
 theorem has_deriv_at_filter.is_O_sub_rev (hf : has_deriv_at_filter f f' x L) (hf' : f' ≠ 0) :
   (λ x', x' - x) =O[L] (λ x', f x' - f x) :=
 suffices antilipschitz_with ∥f'∥₊⁻¹ (smul_right (1 : 𝕜 →L[𝕜] 𝕜) f'), from hf.is_O_sub_rev this,
-(smul_right (1 : 𝕜 →L[𝕜] 𝕜) f').to_linear_map.antilipschitz_of_bound $
+add_monoid_hom_class.antilipschitz_of_bound (smul_right (1 : 𝕜 →L[𝕜] 𝕜) f') $
   λ x, by simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel _ (mt norm_eq_zero.1 hf')]
 
 theorem has_deriv_at_filter.sub_const

src/analysis/calculus/fderiv.lean

@@ -672,7 +672,8 @@ lemma has_fderiv_at_filter.is_O_sub_rev (hf : has_fderiv_at_filter f f' x L) {C}
   (hf' : antilipschitz_with C f') :
   (λ x', x' - x) =O[L] (λ x', f x' - f x) :=
 have (λ x', x' - x) =O[L] (λ x', f' (x' - x)),
-  from is_O_iff.2 ⟨C, eventually_of_forall $ λ x', f'.to_linear_map.bound_of_antilipschitz hf' _⟩,
+  from is_O_iff.2 ⟨C, eventually_of_forall $ λ x',
+    add_monoid_hom_class.bound_of_antilipschitz f' hf' _⟩,
 (this.trans (hf.trans_is_O this).right_is_O_add).congr (λ _, rfl) (λ _, sub_add_cancel _ _)
 
 end continuous

src/analysis/locally_convex/bounded.lean

@@ -106,7 +106,8 @@ lemma is_vonN_bounded.image {σ : 𝕜₁ →+* 𝕜₂} [ring_hom_surjective σ
   is_vonN_bounded 𝕜₂ (f '' s) :=
 begin
   let σ' := ring_equiv.of_bijective σ ⟨σ.injective, σ.is_surjective⟩,
-  have σ_iso : isometry σ := σ.to_add_monoid_hom.isometry_of_norm (λ x, ring_hom_isometric.is_iso),
+  have σ_iso : isometry σ := add_monoid_hom_class.isometry_of_norm σ
+    (λ x, ring_hom_isometric.is_iso),
   have σ'_symm_iso : isometry σ'.symm := σ_iso.right_inv σ'.right_inv,
   have f_tendsto_zero := f.continuous.tendsto 0,
   rw map_zero at f_tendsto_zero,

src/analysis/normed/group/SemiNormedGroup.lean

@@ -56,7 +56,7 @@ lemma is_zero_of_subsingleton (V : SemiNormedGroup) [subsingleton V] :
   limits.is_zero V :=
 begin
   refine ⟨λ X, ⟨⟨⟨0⟩, λ f, _⟩⟩, λ X, ⟨⟨⟨0⟩, λ f, _⟩⟩⟩,
-  { ext, have : x = 0 := subsingleton.elim _ _, simp only [this, normed_group_hom.map_zero], },
+  { ext, have : x = 0 := subsingleton.elim _ _, simp only [this, map_zero], },
   { ext, apply subsingleton.elim }
 end
 
@@ -67,7 +67,7 @@ lemma iso_isometry_of_norm_noninc {V W : SemiNormedGroup} (i : V ≅ W)
   (h1 : i.hom.norm_noninc) (h2 : i.inv.norm_noninc) :
   isometry i.hom :=
 begin
-  apply normed_group_hom.isometry_of_norm,
+  apply add_monoid_hom_class.isometry_of_norm,
   intro v,
   apply le_antisymm (h1 v),
   calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [iso.hom_inv_id_apply]
@@ -153,8 +153,8 @@ lemma is_zero_of_subsingleton (V : SemiNormedGroup₁) [subsingleton V] :
   limits.is_zero V :=
 begin
   refine ⟨λ X, ⟨⟨⟨0⟩, λ f, _⟩⟩, λ X, ⟨⟨⟨0⟩, λ f, _⟩⟩⟩,
-  { ext, have : x = 0 := subsingleton.elim _ _, simp only [this, normed_group_hom.map_zero],
-    apply f.1.map_zero, },
+  { ext, have : x = 0 := subsingleton.elim _ _, simp only [this, map_zero],
+    exact map_zero f.1 },
   { ext, apply subsingleton.elim }
 end
 
@@ -164,7 +164,8 @@ instance has_zero_object : limits.has_zero_object SemiNormedGroup₁.{u} :=
 lemma iso_isometry {V W : SemiNormedGroup₁} (i : V ≅ W) :
   isometry i.hom :=
 begin
-  apply normed_group_hom.isometry_of_norm,
+  change isometry (i.hom : V →+ W),
+  refine add_monoid_hom_class.isometry_of_norm i.hom _,
   intro v,
   apply le_antisymm (i.hom.2 v),
   calc ∥v∥ = ∥i.inv (i.hom v)∥ : by rw [iso.hom_inv_id_apply]

src/analysis/normed/group/SemiNormedGroup/completion.lean

@@ -79,9 +79,9 @@ add_monoid_hom.mk' (category_theory.functor.map Completion) $ λ f g,
 instance : preadditive SemiNormedGroup.{u} :=
 { hom_group := λ P Q, infer_instance,
   add_comp' := by { intros, ext,
-    simp only [normed_group_hom.add_apply, category_theory.comp_apply, normed_group_hom.map_add] },
+    simp only [normed_group_hom.add_apply, category_theory.comp_apply, map_add] },
   comp_add' := by { intros, ext,
-    simp only [normed_group_hom.add_apply, category_theory.comp_apply, normed_group_hom.map_add] } }
+    simp only [normed_group_hom.add_apply, category_theory.comp_apply, map_add] } }
 
 instance : functor.additive Completion :=
 { map_add' := λ X Y, (Completion.map_hom _ _).map_add }

src/analysis/normed/group/basic.lean

@@ -461,9 +461,9 @@ open finset
 /-- A homomorphism `f` of seminormed groups is Lipschitz, if there exists a constant `C` such that
 for all `x`, one has `∥f x∥ ≤ C * ∥x∥`. The analogous condition for a linear map of
 (semi)normed spaces is in `normed_space.operator_norm`. -/
-lemma add_monoid_hom.lipschitz_of_bound (f : E →+ F) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
-  lipschitz_with (real.to_nnreal C) f :=
-lipschitz_with.of_dist_le' $ λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
+lemma add_monoid_hom_class.lipschitz_of_bound {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F] (f : 𝓕)
+  (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : lipschitz_with (real.to_nnreal C) f :=
+lipschitz_with.of_dist_le' $ λ x y, by simpa only [dist_eq_norm, map_sub] using h (x - y)
 
 lemma lipschitz_on_with_iff_norm_sub_le {f : E → F} {C : ℝ≥0} {s : set E} :
   lipschitz_on_with C f s ↔  ∀ (x ∈ s) (y ∈ s), ∥f x - f y∥ ≤ C * ∥x - y∥ :=
@@ -490,11 +490,14 @@ lemma lipschitz_with.norm_sub_le_of_le {f : E → F} {C : ℝ≥0} (h : lipschit
 (h.norm_sub_le x y).trans $ mul_le_mul_of_nonneg_left hd C.2
 
 /-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant `C` such that
-for all `x`, one has `∥f x∥ ≤ C * ∥x∥`.
-The analogous condition for a linear map of normed spaces is in `normed_space.operator_norm`. -/
-lemma add_monoid_hom.continuous_of_bound (f : E →+ F) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
-  continuous f :=
-(f.lipschitz_of_bound C h).continuous
+for all `x`, one has `∥f x∥ ≤ C * ∥x∥`.  -/
+lemma add_monoid_hom_class.continuous_of_bound {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F] (f : 𝓕)
+  (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : continuous f :=
+(add_monoid_hom_class.lipschitz_of_bound f C h).continuous
+
+lemma add_monoid_hom_class.uniform_continuous_of_bound {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F]
+  (f : 𝓕) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : uniform_continuous f :=
+(add_monoid_hom_class.lipschitz_of_bound f C h).uniform_continuous
 
 lemma is_compact.exists_bound_of_continuous_on [topological_space α]
   {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous_on f s) :
@@ -505,15 +508,17 @@ begin
   exact ⟨C, λ x hx, hC _ (set.mem_image_of_mem _ hx)⟩,
 end
 
-lemma add_monoid_hom.isometry_iff_norm (f : E →+ F) : isometry f ↔ ∀ x, ∥f x∥ = ∥x∥ :=
+lemma add_monoid_hom_class.isometry_iff_norm {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F]
+  (f : 𝓕) : isometry f ↔ ∀ x, ∥f x∥ = ∥x∥ :=
 begin
-  simp only [isometry_emetric_iff_metric, dist_eq_norm, ← f.map_sub],
+  simp only [isometry_emetric_iff_metric, dist_eq_norm, ←map_sub],
   refine ⟨λ h x, _, λ h x y, h _⟩,
   simpa using h x 0
 end
 
-lemma add_monoid_hom.isometry_of_norm (f : E →+ F) (hf : ∀ x, ∥f x∥ = ∥x∥) : isometry f :=
-f.isometry_iff_norm.2 hf
+lemma add_monoid_hom_class.isometry_of_norm {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F]
+  (f : 𝓕) (hf : ∀ x, ∥f x∥ = ∥x∥) : isometry f :=
+(add_monoid_hom_class.isometry_iff_norm f).2 hf
 
 lemma controlled_sum_of_mem_closure {s : add_subgroup E} {g : E}
   (hg : g ∈ closure (s : set E)) {b : ℕ → ℝ} (b_pos : ∀ n, 0 < b n) :
@@ -652,9 +657,20 @@ lemma nnnorm_sum_le_of_le (s : finset ι) {f : ι → E} {n : ι → ℝ≥0} (h
   ∥∑ b in s, f b∥₊ ≤ ∑ b in s, n b :=
 (norm_sum_le_of_le s h).trans_eq nnreal.coe_sum.symm
 
-lemma add_monoid_hom.lipschitz_of_bound_nnnorm (f : E →+ F) (C : ℝ≥0) (h : ∀ x, ∥f x∥₊ ≤ C * ∥x∥₊) :
-  lipschitz_with C f :=
-@real.to_nnreal_coe C ▸ f.lipschitz_of_bound C h
+lemma add_monoid_hom_class.lipschitz_of_bound_nnnorm {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F]
+  (f : 𝓕) (C : ℝ≥0) (h : ∀ x, ∥f x∥₊ ≤ C * ∥x∥₊) : lipschitz_with C f :=
+@real.to_nnreal_coe C ▸ add_monoid_hom_class.lipschitz_of_bound f C h
+
+lemma add_monoid_hom_class.antilipschitz_of_bound {𝓕 : Type*}
+  [add_monoid_hom_class 𝓕 E F] (f : 𝓕) {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤ K * ∥f x∥) :
+  antilipschitz_with K f :=
+antilipschitz_with.of_le_mul_dist $
+λ x y, by simpa only [dist_eq_norm, map_sub] using h (x - y)
+
+lemma add_monoid_hom_class.bound_of_antilipschitz {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F] (f : 𝓕)
+  {K : ℝ≥0} (h : antilipschitz_with K f) (x) : ∥x∥ ≤ K * ∥f x∥ :=
+by simpa only [dist_zero_right, map_zero] using h.le_mul_dist x 0
+
 
 end nnnorm
 

src/analysis/normed/group/hom.lean

@@ -107,25 +107,19 @@ lemma to_add_monoid_hom_injective :
 @[simp] lemma mk_to_add_monoid_hom (f) (h₁) (h₂) :
   (⟨f, h₁, h₂⟩ : normed_group_hom V₁ V₂).to_add_monoid_hom = add_monoid_hom.mk' f h₁ := rfl
 
-@[simp] lemma map_zero : f 0 = 0 := f.to_add_monoid_hom.map_zero
-
-@[simp] lemma map_add (x y) : f (x + y) = f x + f y := f.to_add_monoid_hom.map_add _ _
-
-@[simp] lemma map_sum {ι : Type*} (v : ι → V₁) (s : finset ι) :
-  f (∑ i in s, v i) = ∑ i in s, f (v i) :=
-f.to_add_monoid_hom.map_sum _ _
-
-@[simp] lemma map_sub (x y) : f (x - y) = f x - f y := f.to_add_monoid_hom.map_sub _ _
-
-@[simp] lemma map_neg (x) : f (-x) = -(f x) := f.to_add_monoid_hom.map_neg _
+instance : add_monoid_hom_class (normed_group_hom V₁ V₂) V₁ V₂ :=
+{ coe := coe_fn,
+  coe_injective' := coe_injective,
+  map_add := λ f, f.to_add_monoid_hom.map_add,
+  map_zero := λ f, f.to_add_monoid_hom.map_zero }
 
 lemma bound : ∃ C, 0 < C ∧ ∀ x, ∥f x∥ ≤ C * ∥x∥ :=
 let ⟨C, hC⟩ := f.bound' in exists_pos_bound_of_bound _ hC
 
 theorem antilipschitz_of_norm_ge {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤ K * ∥f x∥) :
   antilipschitz_with K f :=
 antilipschitz_with.of_le_mul_dist $
-λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
+λ x y, by simpa only [dist_eq_norm, map_sub] using h (x - y)
 
 /-- A normed group hom is surjective on the subgroup `K` with constant `C` if every element
 `x` of `K` has a preimage whose norm is bounded above by `C*∥x∥`. This is a more
@@ -226,7 +220,7 @@ le_antisymm (f.op_norm_le_bound M_nonneg h_above)
 
 theorem op_norm_le_of_lipschitz {f : normed_group_hom V₁ V₂} {K : ℝ≥0} (hf : lipschitz_with K f) :
   ∥f∥ ≤ K :=
-f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0
+f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0
 
 /-- If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
 `mk_normed_group_hom`, then its norm is bounded by the bound given to the constructor if it is
@@ -379,7 +373,7 @@ instance : has_scalar R (normed_group_hom V₁ V₂) :=
     map_add' := (r • f.to_add_monoid_hom).map_add',
     bound' := let ⟨b, hb⟩ := f.bound' in  ⟨dist r 0 * b, λ x, begin
       have := dist_smul_pair r (f x) (f 0),
-      rw [f.map_zero, smul_zero, dist_zero_right, dist_zero_right] at this,
+      rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this,
       rw mul_assoc,
       refine this.trans _,
       refine mul_le_mul_of_nonneg_left _ dist_nonneg,
@@ -494,12 +488,12 @@ by { rw h, exact norm_comp_le_of_le hg hf }
 /-- Composition of normed groups hom as an additive group morphism. -/
 def comp_hom : (normed_group_hom V₂ V₃) →+ (normed_group_hom V₁ V₂) →+ (normed_group_hom V₁ V₃) :=
 add_monoid_hom.mk' (λ g, add_monoid_hom.mk' (λ f, g.comp f)
-  (by { intros, ext, exact g.map_add _ _ }))
+  (by { intros, ext, exact map_add g _ _ }))
   (by { intros, ext, simp only [comp_apply, pi.add_apply, function.comp_app,
                                 add_monoid_hom.add_apply, add_monoid_hom.mk'_apply, coe_add] })
 
 @[simp] lemma comp_zero (f : normed_group_hom V₂ V₃) : f.comp (0 : normed_group_hom V₁ V₂) = 0 :=
-by { ext, exact f.map_zero }
+by { ext, exact map_zero f }
 
 @[simp] lemma zero_comp (f : normed_group_hom V₁ V₂) : (0 : normed_group_hom V₂ V₃).comp f = 0 :=
 by { ext, refl }
@@ -626,17 +620,9 @@ end norm_noninc
 
 section isometry
 
-lemma isometry_iff_norm (f : normed_group_hom V W) :
-  isometry f ↔ ∀ v, ∥f v∥ = ∥v∥ :=
-add_monoid_hom.isometry_iff_norm f.to_add_monoid_hom
-
-lemma isometry_of_norm (f : normed_group_hom V W) (hf : ∀ v, ∥f v∥ = ∥v∥) :
-  isometry f :=
-f.isometry_iff_norm.mpr hf
-
 lemma norm_eq_of_isometry {f : normed_group_hom V W} (hf : isometry f) (v : V) :
   ∥f v∥ = ∥v∥ :=
-f.isometry_iff_norm.mp hf v
+(add_monoid_hom_class.isometry_iff_norm f).mp hf v
 
 lemma isometry_id : @isometry V V _ _ (id V) :=
 isometry_id
@@ -799,7 +785,7 @@ begin
   { /- We indeed get a preimage. First note: -/
     have : f ∘ s = λ n, ∑ k in range (n + 1), v k,
     { ext n,
-      simp [f.map_sum, hu] },
+      simp [map_sum, hu] },
     /- In the above equality, the left-hand-side converges to `f g` by continuity of `f` and
        definition of `g` while the right-hand-side converges to `h` by construction of `v` so
        `g` is indeed a preimage of `h`. -/

src/analysis/normed/group/hom_completion.lean

@@ -202,13 +202,13 @@ begin
     obtain ⟨g' : G, hgg' : f g' = f g, hfg : ∥g'∥ ≤ C' * ∥f g∥⟩ :=
       hC' (f g) (mem_range_self g),
     have mem_ker : g - g' ∈ f.ker,
-      by rw [f.mem_ker, f.map_sub, sub_eq_zero.mpr hgg'.symm],
+      by rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm],
     have : ∥f g∥ ≤ ∥f∥*∥hatg - g∥,
     calc
       ∥f g∥ = ∥f.completion g∥ : by rw [f.completion_coe, completion.norm_coe]
         ... = ∥f.completion g - 0∥ : by rw [sub_zero _]
         ... = ∥f.completion g - (f.completion hatg)∥ : by rw [(f.completion.mem_ker _).mp hatg_in]
-        ... = ∥f.completion (g - hatg)∥ : by rw [f.completion.map_sub]
+        ... = ∥f.completion (g - hatg)∥ : by rw [map_sub]
         ... ≤ ∥f.completion∥ * ∥(g :completion G) - hatg∥ : f.completion.le_op_norm _
         ... = ∥f∥ * ∥hatg - g∥ : by rw [norm_sub_rev, f.norm_completion],
     have : ∥(g' : completion G)∥ ≤ C'*∥f∥*∥hatg - g∥,

src/analysis/normed/group/quotient.lean

@@ -475,7 +475,7 @@ begin
     exact ⟨0, f.ker.zero_mem⟩ },
   rcases real.lt_Inf_add_pos nonemp hε with
     ⟨_, ⟨⟨x, hx, rfl⟩, H : ∥m + x∥ < Inf ((λ (m' : M), ∥m + m'∥) '' f.ker) + ε⟩⟩,
-  exact ⟨m+x, by rw [f.map_add,(normed_group_hom.mem_ker f x).mp hx, add_zero],
+  exact ⟨m+x, by rw [map_add,(normed_group_hom.mem_ker f x).mp hx, add_zero],
                by rwa hquot.norm⟩,
 end
 

src/analysis/normed_space/banach_steinhaus.lean

@@ -119,7 +119,7 @@ def continuous_linear_map_of_tendsto [complete_space E] [t2_space F]
       cases banach_steinhaus h_point_bdd with C' hC',
       /- show the uniform bound from `banach_steinhaus` is a norm bound of the limit map
          by allowing "an `ε` of room." -/
-      refine linear_map.continuous_of_bound (linear_map_of_tendsto _ _ h) C'
+      refine add_monoid_hom_class.continuous_of_bound (linear_map_of_tendsto _ _ h) C'
         (λ x, le_of_forall_pos_lt_add (λ ε ε_pos, _)),
       cases metric.tendsto_at_top.mp (tendsto_pi_nhds.mp h x) ε ε_pos with n hn,
       have lt_ε : ∥g n x - f x∥ < ε, by {rw ←dist_eq_norm, exact hn n (le_refl n)},

src/analysis/normed_space/bounded_linear_maps.lean

@@ -87,7 +87,8 @@ def to_linear_map (f : E → F) (h : is_bounded_linear_map 𝕜 f) : E →ₗ[
 
 /-- Construct a continuous linear map from is_bounded_linear_map -/
 def to_continuous_linear_map {f : E → F} (hf : is_bounded_linear_map 𝕜 f) : E →L[𝕜] F :=
-{ cont := let ⟨C, Cpos, hC⟩ := hf.bound in (to_linear_map f hf).continuous_of_bound C hC,
+{ cont := let ⟨C, Cpos, hC⟩ :=
+    hf.bound in add_monoid_hom_class.continuous_of_bound (to_linear_map f hf) C hC,
   ..to_linear_map f hf}
 
 lemma zero : is_bounded_linear_map 𝕜 (λ (x:E), (0:F)) :=

src/analysis/normed_space/dual.lean

@@ -47,7 +47,8 @@ variables (F : Type*) [normed_group F] [normed_space 𝕜 F]
 /-- The topological dual of a seminormed space `E`. -/
 @[derive [inhabited, semi_normed_group, normed_space 𝕜]] def dual := E →L[𝕜] 𝕜
 
-instance : add_monoid_hom_class (dual 𝕜 E) E 𝕜 := continuous_linear_map.add_monoid_hom_class
+instance : continuous_linear_map_class (dual 𝕜 E) 𝕜 E 𝕜 :=
+continuous_linear_map.continuous_semilinear_map_class
 
 instance : has_coe_to_fun (dual 𝕜 E) (λ _, E → 𝕜) := continuous_linear_map.to_fun
 

src/analysis/normed_space/finite_dimension.lean

@@ -553,10 +553,10 @@ def continuous_linear_equiv.pi_ring (ι : Type*) [fintype ι] [decidable_eq ι]
   end,
   continuous_inv_fun :=
   begin
-    simp_rw [linear_equiv.inv_fun_eq_symm],
-    apply linear_map.continuous_of_bound _ (fintype.card ι : ℝ) (λ g, _),
-    convert_to ∥linear_map.to_continuous_linear_map.to_linear_map.comp
-                  (linear_equiv.pi_ring 𝕜 E ι 𝕜).symm.to_linear_map g∥ ≤ _,
+    simp_rw [linear_equiv.inv_fun_eq_symm, linear_equiv.trans_symm, linear_equiv.symm_symm],
+    change continuous (linear_map.to_continuous_linear_map.to_linear_map.comp
+                      (linear_equiv.pi_ring 𝕜 E ι 𝕜).symm.to_linear_map),
+    apply add_monoid_hom_class.continuous_of_bound _ (fintype.card ι : ℝ) (λ g, _),
     rw ← nsmul_eq_mul,
     apply op_norm_le_bound _ (nsmul_nonneg (norm_nonneg g) (fintype.card ι)) (λ t, _),
     simp_rw [linear_map.coe_comp, linear_equiv.coe_to_linear_map, function.comp_app,

src/analysis/normed_space/linear_isometry.lean

@@ -105,7 +105,7 @@ f.to_linear_map.map_smul c x
 @[simp] lemma nnnorm_map (x : E) : ∥f x∥₊ = ∥x∥₊ := nnreal.eq $ f.norm_map x
 
 protected lemma isometry : isometry f :=
-f.to_linear_map.to_add_monoid_hom.isometry_of_norm f.norm_map
+add_monoid_hom_class.isometry_of_norm _ (norm_map _)
 
 @[simp] lemma is_complete_image_iff {s : set E} : is_complete (f '' s) ↔ is_complete s :=
 is_complete_image_iff f.isometry.uniform_inducing
@@ -133,6 +133,11 @@ protected lemma antilipschitz : antilipschitz_with 1 f := f.isometry.antilipschi
 
 @[continuity] protected lemma continuous : continuous f := f.isometry.continuous
 
+instance : continuous_semilinear_map_class (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ :=
+{ map_smulₛₗ := λ f, f.map_smulₛₗ,
+  map_continuous := λ f, f.continuous,
+  ..linear_isometry.add_monoid_hom_class }
+
 lemma ediam_image (s : set E) : emetric.diam (f '' s) = emetric.diam s :=
 f.isometry.ediam_image s