Theorems · Theorem · functional analysis

SeparationQuotient.norm_liftNormedAddGroupHom_le

∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0), ‖SeparationQuotient.liftNormedAddGroupHom f hf‖ ≤ ‖f‖

For a norm-continuous group homomorphism f, its lift to the separation quotient is bounded by the norm of f.

Defined in

Mathlib.Analysis.Normed.Group.SeparationQuotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup