Theorems · Definition · functional analysis

NormedAddGroupHom.Equalizer.liftEquiv

{V : Type u_1} →
  {W : Type u_2} →
    {V₁ : Type u_3} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : SeminormedAddCommGroup V₁] →
            {f g : NormedAddGroupHom V W} → { φ // f.comp φ = g.comp φ } ≃ NormedAddGroupHom V₁ ↥(f.equalizer g)

The lifting property of the equalizer as an equivalence.

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroup