opENorm_comp_le — Mathlib

English

Under suitable lower and upper bound hypotheses, the operator norm equals the bound M.

Русский

При подходящих условиях нижней и верхней границ норма оператора равна M.

LaTeX

$$Eq (‖φ‖₊) M under bounds$$

Lean4

theorem opENorm_comp_le (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖h.comp f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ := by
  simpa [enorm, ← ENNReal.coe_mul] using opNNNorm_comp_le h f

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