curry_uncurryRight — Mathlib

English

The curry-right operation preserves the operator norm, i.e., ‖f.curryRight‖ = ‖f‖.

Русский

Операция curryRight сохраняет норму: ‖f.curryRight‖ = ‖f‖.

LaTeX

$$$\|f.curryRight\| = \|f\|$$$

Lean4

@[simp]
theorem curry_uncurryRight (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G)) :
    f.uncurryRight.curryRight = f := by
  ext m x
  rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply, snoc_last, init_snoc]

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