Theorems · Theorem · functional analysis

NormedAddGroupHom.comp_assoc

∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {V₄ : Type u_5}
  [inst_3 : SeminormedAddCommGroup V₄] (h : NormedAddGroupHom V₃ V₄) (g : NormedAddGroupHom V₂ V₃)
  (f : NormedAddGroupHom V₁ V₂), (h.comp g).comp f = h.comp (g.comp f)

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroup