Theorems · Theorem · functional analysis

NormedAddGroupHom.Equalizer.map_normNoninc

∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {W₁ : Type u_6} {W₂ : Type u_7} [inst_2 : SeminormedAddCommGroup W₁] [inst_3 : SeminormedAddCommGroup W₂]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂}
  {ψ : NormedAddGroupHom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ),
  φ.NormNoninc → (NormedAddGroupHom.Equalizer.map φ ψ hf hg).NormNoninc

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroup