Theorems · Theorem · functional analysis

ContinuousLinearMap.opNNNorm_comp_linearIsometryEquiv

∀ {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜₁] [inst_4 : NormedSpace 𝕜₁ E] [inst_5 : NontriviallyNormedField 𝕜₂]
  [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : NontriviallyNormedField 𝕜₃] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜₁} [inst_9 : RingHomInvPair σ₁₂ σ₂₁] [inst_10 : RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜₁ →+* 𝕜₃} [inst_11 : RingHomIsometric σ₁₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_13 : RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F), ‖f ∘SL ↑↑e‖₊ = ‖f‖₊

Precomposition with a linear isometry preserves the operator norm.

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

2 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNontriviallyNormedFieldNormedSpaceNontriviallyNormedFieldNormedSpaceNontriviallyNormedFieldNormedSpaceRingHomInvPairRingHomInvPairRingHomIsometricRingHomCompTripleRingHomIsometric