curryLeft_norm — Mathlib

English

Bounds for the init component input of a continuous multilinear map, in terms of ‖f‖ and the product of norms of inputs.

Русский

Ограничение для входа init компоненты непрерывного многолинейного отображения через ‖f‖ и произведение норм входов.

LaTeX

$$$\|f( init\; m)( last )\| \leq \|f\| \cdot \prod_i \|m_i\|$$$

Lean4

@[simp]
theorem curryLeft_norm (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖f.curryLeft‖ = ‖f‖ :=
  (continuousMultilinearCurryLeftEquiv 𝕜 Ei G).norm_map f

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