Theorems · Theorem · functional analysis

ContinuousLinearMap.bilinearComp.congr_simp

∀ {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  (f f_1 : E →SL[σ₁₃] F →SL[σ₂₃] G),
  f = f_1 →
    ∀ (gE gE_1 : E' →SL[σ₁'] E),
      gE = gE_1 → ∀ (gF gF_1 : F' →SL[σ₂'] F), gF = gF_1 → f.bilinearComp gE gF = f_1.bilinearComp gE_1 gF_1

Defined in

Mathlib.Analysis.Normed.Operator.Bilinear

Cited by

5 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceNormedSpaceNormedSpaceSeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceNormedSpaceRingHomCompTripleRingHomCompTripleRingHomIsometricRingHomIsometricRingHomIsometric