norm_precompR_le — Mathlib

English

For any L, the operator norm of the right precomposition precompR Eℓ L is at most the operator norm of L: ||precompR Eℓ L|| ≤ ||L||.

Русский

Для любого L нормa оператора правой пре-композиции удовлетворяет: ||precompR Eℓ L|| ≤ ||L||.

LaTeX

$$$\|\mathrm{precompR}_{E_\ell} L\| \leq \|L\|$$$

Lean4

theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖ :=
  calc
    ‖precompR Eₗ L‖ ≤ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ * ‖L‖ := opNorm_comp_le _ _
    _ ≤ 1 * ‖L‖ := by gcongr; apply norm_compL_le
    _ = ‖L‖ := by rw [one_mul]

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