Theorems · Theorem · functional analysis

ContinuousLinearMapWOT.comp_assoc

∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {𝕜₄ : Type u_8} {E : Type u_9} {F : Type u_10} {G : Type u_11}
  {H : Type u_12} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : NormedField 𝕜₄]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₁₄ : 𝕜₁ →+* 𝕜₄} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₃₄ : 𝕜₃ →+* 𝕜₄}
  [inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_5 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_6 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_7 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_8 : AddCommGroup E]
  [inst_9 : TopologicalSpace E] [inst_10 : Module 𝕜₁ E] [inst_11 : AddCommGroup F] [inst_12 : TopologicalSpace F]
  [inst_13 : Module 𝕜₂ F] [inst_14 : AddCommGroup G] [inst_15 : TopologicalSpace G] [inst_16 : Module 𝕜₃ G]
  [inst_17 : AddCommGroup H] [inst_18 : TopologicalSpace H] [inst_19 : Module 𝕜₄ H] (g₃₄ : G →SWOT[σ₃₄] H)
  (g₂₃ : F →SWOT[σ₂₃] G) (g₁₂ : E →SWOT[σ₁₂] F), (g₃₄.comp g₂₃).comp g₁₂ = g₃₄.comp (g₂₃.comp g₁₂)

Defined in

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

NormedFieldNormedFieldNormedFieldNormedFieldRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleAddCommGroupTopologicalSpaceModuleAddCommGroupTopologicalSpaceModuleAddCommGroupTopologicalSpaceModuleAddCommGroupTopologicalSpaceModule