Theorems · Theorem · functional analysis

NormedAddGroupHom.Equalizer.map_comp_map

∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7}
  {W₃ : Type u_8} [inst_3 : SeminormedAddCommGroup W₁] [inst_4 : SeminormedAddCommGroup W₂]
  [inst_5 : SeminormedAddCommGroup W₃] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂}
  {f₃ g₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂}
  {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ)
  (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ'),
  (NormedAddGroupHom.Equalizer.map φ' ψ' hf' hg').comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) =
    NormedAddGroupHom.Equalizer.map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroup