Theorems · Theorem · functional analysis

QuotientAddGroup.norm_lift_apply_le

∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {S : AddSubgroup M} (f : NormedAddGroupHom M N) (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S),
  ‖(QuotientAddGroup.lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Defined in

Mathlib.Analysis.Normed.Group.Quotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup