uncurryRight_norm — Mathlib

English

The operation of uncurryRight preserves the operator norm: ∥f.uncurryRight∥ = ∥f∥.

Русский

Нормa оператора сохраняется при uncurryRight: ∥f.uncurryRight∥ = ∥f∥.

LaTeX

$$$\\|f.uncurryRight\\| = \\|f\\|$$$

Lean4

@[simp]
theorem uncurryRight_norm (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G)) :
    ‖f.uncurryRight‖ = ‖f‖ :=
  (continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm.norm_map f

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