chore(analysis/normed_space/pi_Lp): add `pi_Lp.continuous_linear_equi…

…v` (#19014)

This bundling is often useful to have.
We keep around `pi_Lp.linear_equiv` as this is shorter to write than `pi_Lp.continuous_linear_equiv.to_linear_equiv`.

src/analysis/normed_space/pi_Lp.lean

@@ -707,13 +707,20 @@ lemma norm_equiv_symm_one {β} [seminormed_add_comm_group β] (hp : p ≠ ∞) [
 
 variables (𝕜 p)
 
-/-- `pi_Lp.equiv` as a linear map. -/
+/-- `pi_Lp.equiv` as a linear equivalence. -/
 @[simps {fully_applied := ff}]
 protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
 { to_fun := pi_Lp.equiv _ _,
   inv_fun := (pi_Lp.equiv _ _).symm,
   ..linear_equiv.refl _ _}
 
+/-- `pi_Lp.equiv` as a continuous linear equivalence. -/
+@[simps {fully_applied := ff}]
+protected def continuous_linear_equiv : pi_Lp p β ≃L[𝕜] Π i, β i :=
+{ to_linear_equiv := pi_Lp.linear_equiv _ _ _,
+  continuous_to_fun := continuous_equiv _ _,
+  continuous_inv_fun := continuous_equiv_symm _ _ }
+
 section basis
 
 variables (ι)