Theorems · Definition · functional analysis

NormedAddGroupHom.extension

{G : Type u_1} →
  [inst : SeminormedAddCommGroup G] →
    {H : Type u_2} →
      [inst_1 : SeminormedAddCommGroup H] →
        [T0Space H] → [CompleteSpace H] → NormedAddGroupHom G H → NormedAddGroupHom (UniformSpace.Completion G) H

If H is complete, the extension of f : NormedAddGroupHom G H to a NormedAddGroupHom (completion G) H.

Defined in

Mathlib.Analysis.Normed.Group.HomCompletion

Cited by

4 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupT0SpaceCompleteSpace