map_normNoninc — Mathlib

English

The induced map on the equalizer, constructed from φ and ψ, is norm-nonincreasing whenever φ is norm-nonincreasing and the defining equalities hold.

Русский

Полученная из φ и ψ карта на равновесии не увеличивает норму, если φ не возрастает по норме и выполняются соответствующие равенства.

LaTeX

$$$\| \mathrm{map}(\varphi,\psi;hf,hg) \| \le 1.$$$

Lean4

theorem map_normNoninc (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.NormNoninc) :
    (map φ ψ hf hg).NormNoninc :=
  lift_normNoninc _ _ <| hφ.comp ι_normNoninc

Похожие утверждения