uncurryRight_apply — Mathlib

English

Bounding the norm of f after inserting an element into a coordinate slot: the result is bounded by ‖f‖, the norm of the inserted element, and the product of norms of other coordinates.

Русский

Граница нормы после вставки элемента в координатную позицию: равна ≤ ‖f‖ · ‖x‖ · ∏ ‖m_i‖.

LaTeX

$$$\|f( i.insertNth x m )\| \leq \|f\| \cdot \|x\| \cdot \prod_j \|m_j\|$$$

Lean4

@[simp]
theorem uncurryRight_apply (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G))
    (m : ∀ i, Ei i) : f.uncurryRight m = f (init m) (m (last n)) :=
  rfl

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