ContinuousLinearMap.opNorm_flip

theorem ContinuousLinearMap.opNorm_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G] [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃] [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), ‖f.flip‖ = ‖f‖

The theorem `ContinuousLinearMap.opNorm_flip` states that for any continuous linear map `f`, which is a map from a normed space `E` over a nontrivially normed field `𝕜` to a continuous linear map from a normed space `F` over a nontrivially normed field `𝕜₂` to a normed space `G` over a nontrivially normed field `𝕜₃` (where the field homomorphisms from `𝕜` to `𝕜₃` and `𝕜₂` to `𝕜₃` are isometric), the operator norm of the flip of `f` is equal to the operator norm of `f`. The flip of a continuous linear map is a function that reverses the order of the two spaces the map operates on.

More concisely: For any continuous linear map $f$ from a normed space $E$ over a nontrivially normed field $\mathbb{K}$ to a continuous linear map from a normed space $F$ over $\mathbb{K}$ to a normed space $G$ over $\mathbb{K}$ (with isometric field homomorphisms from $\mathbb{K}$ to the fields of $F$ and $G$), the operator norms of $f$ and its flip are equal.