feat(analysis/normed_space/operator_norm): construct a continuous_lin…

…ear_equiv from a linear_equiv and bounds in both directions (#4583)

src/analysis/normed_space/operator_norm.lean

@@ -900,6 +900,14 @@ continuous_linear_equiv.uniform_embedding
   continuous_inv_fun := h₂,
   .. e }
 
+/-- Construct a continuous linear equivalence from a linear equivalence together with
+bounds in both directions. -/
+def linear_equiv.to_continuous_linear_equiv_of_bounds (e : E ≃ₗ[𝕜] F) (C_to C_inv : ℝ)
+  (h_to : ∀ x, ∥e x∥ ≤ C_to * ∥x∥) (h_inv : ∀ x : F, ∥e.symm x∥ ≤ C_inv * ∥x∥) : E ≃L[𝕜] F :=
+{ to_linear_equiv := e,
+  continuous_to_fun := e.to_linear_map.continuous_of_bound C_to h_to,
+  continuous_inv_fun := e.symm.to_linear_map.continuous_of_bound C_inv h_inv }
+
 namespace continuous_linear_map
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']