norm_map_le — Mathlib

English

If the composed norm of ι with φ is bounded by C, then the norm of the lifted morphism is also bounded by C: ‖lift φ h‖ ≤ C.

Русский

Если ‖φ ∘ ι‖ ≤ C, тогда ‖lift φ h‖ ≤ C.

LaTeX

$$$\| \mathrm{lift}(\varphi,h) \| \le C \quad \text{whenever } \| \varphi \circ \iota \| \le C.$$$

Lean4

theorem norm_map_le (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ℝ) (hφ : ‖φ.comp (ι f₁ g₁)‖ ≤ C) :
    ‖map φ ψ hf hg‖ ≤ C :=
  norm_lift_le _ _ _ hφ

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