le_opNNNorm — Mathlib

English

The operator norm of the zero map is zero.

Русский

Норма оператора нулевого отображения равна нулю.

LaTeX

$$$$ \\|0\\| = 0.$$$$

Lean4

/-- The fundamental property of the operator norm of a continuous multilinear map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`, `nnnorm` version. -/
theorem le_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact f.le_opNorm m

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