Theorems · Definition · functional analysis

NormedAddGroupHom.lift

{M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {N : Type u_3} →
      [inst_1 : SeminormedAddCommGroup N] →
        (S : AddSubgroup M) → (f : NormedAddGroupHom M N) → (∀ s ∈ S, f s = 0) → NormedAddGroupHom (M ⧸ S) N

Given f : NormedAddGroupHom M N such that f s = 0 for all s ∈ S, where, S : AddSubgroup M is closed, the induced morphism NormedAddGroupHom (M ⧸ S) N.

Defined in

Mathlib.Analysis.Normed.Group.Quotient

Cited by

6 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup