uncurryLeft_norm — Mathlib

English

Bound for tail coordinate evaluation of multilinear map: the tail input norm multiplies into the bound with ‖f‖ and ∏ ‖m_i‖.

Русский

Граница для tail-координат: нормa хвоста входит в ограничение вместе с ‖f‖ и произведением ‖m_i‖.

LaTeX

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

Lean4

@[simp]
theorem uncurryLeft_norm (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) :
    ‖f.uncurryLeft‖ = ‖f‖ :=
  (continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm.norm_map f

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