norm_mkPiAlgebraFin_zero — Mathlib

English

For a multilinear map f and a vector z, the NN-norm of the result of applying f to z (smulRight) equals the product of the NN-norms: the NN-norm of f times the NN-norm of z.

Русский

Для отображения f и вектора z норма NN результата применения f к z равна произведению NN-норм f и NN-норм z.

LaTeX

$$$\|f \!\cdot\! z\|_{\mathrm{nn}} = \|f\|_{\mathrm{nn}} \cdot \|z\|_{\mathrm{nn}}$$$

Lean4

theorem norm_mkPiAlgebraFin_zero : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖(1 : A)‖ :=
  by
  refine le_antisymm ?_ ?_
  · refine opNorm_le_bound (norm_nonneg (1 : A)) ?_
    simp
  · convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)
    simp

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