opNorm_prod — Mathlib

English

The formula for prodMapL on a pair p is p.1.prodMap p.2.

Русский

Формула для prodMapL на пары p: p.1.prodMap p.2.

LaTeX

$$$$\\mathrm{prodMapL}(\\mathbb{K})~p = p.1.\\mathrm{prodMap}~p.2.$$$$

Lean4

@[simp]
theorem opNorm_prod (f : E →L[𝕜] F) (g : E →L[𝕜] G) : ‖f.prod g‖ = ‖(f, g)‖ :=
  le_antisymm
      (opNorm_le_bound _ (norm_nonneg _) fun x => by
        simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, norm_nonneg] using
          max_le_max (le_opNorm f x) (le_opNorm g x)) <|
    max_le (opNorm_le_bound _ (norm_nonneg _) fun x => (le_max_left _ _).trans ((f.prod g).le_opNorm x))
      (opNorm_le_bound _ (norm_nonneg _) fun x => (le_max_right _ _).trans ((f.prod g).le_opNorm x))

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