lift_normNoninc — Mathlib

English

The lifting construction preserves norm nonincreasing behavior: if φ is a norm-nonincreasing morphism and φ composes equally through f and g, then the lift φ h is norm-nonincreasing.

Русский

Пусть φ—гомоморфизм с невозрастающей нормой и f ∘ φ = g ∘ φ. Тогда подъем (lift) φ, h является нормой не возрастает.

LaTeX

$$$\| \mathrm{lift}(\varphi,h) \| \le 1 \quad \text{whenever } \| \varphi \| \le 1 \text{ and } f \circ \varphi = g \circ \varphi.$$$

Lean4

/-- The lifting of a norm nonincreasing morphism is norm nonincreasing. -/
theorem lift_normNoninc (φ : NormedAddGroupHom V₁ V) (h : f.comp φ = g.comp φ) (hφ : φ.NormNoninc) :
    (lift φ h).NormNoninc :=
  hφ

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