Theorems · Theorem · functional analysis

SeparationQuotient.norm_liftNormedAddGroupHom_apply_le

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

Defined in

Mathlib.Analysis.Normed.Group.SeparationQuotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup