Theorems · Definition · functional analysis

NormedAddGroupHom.ker.lift

{V₁ : Type u_3} →
  {V₂ : Type u_4} →
    {V₃ : Type u_5} →
      [inst : SeminormedAddCommGroup V₁] →
        [inst_1 : SeminormedAddCommGroup V₂] →
          [inst_2 : SeminormedAddCommGroup V₃] →
            (f : NormedAddGroupHom V₁ V₂) → (g : NormedAddGroupHom V₂ V₃) → g.comp f = 0 → NormedAddGroupHom V₁ ↥g.ker

Given a normed group hom f : V₁ → V₂ satisfying g.comp f = 0 for some g : V₂ → V₃, the corestriction of f to the kernel of g.

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroup