Theorems · Definition · functional analysis

SeparationQuotient.liftNormedAddGroupHom

{M : Type u_1} →
  {N : Type u_2} →
    [inst : SeminormedAddCommGroup M] →
      [inst_1 : SeminormedAddCommGroup N] →
        (f : NormedAddGroupHom M N) → (∀ (x : M), ‖x‖ = 0 → f x = 0) → NormedAddGroupHom (SeparationQuotient M) N

The lift of a group hom to the separation quotient as a group hom.

Defined in

Mathlib.Analysis.Normed.Group.SeparationQuotient

Cited by

6 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup