curryRight_norm — Mathlib

English

The operation of currying on the right does not change the operator norm: the norm of f.curryRight equals the norm of f.

Русский

Операция правого каррирования не изменяет операторную норму: ∥f.curryRight∥ = ∥f∥.

LaTeX

$$$\\|f.\\text{curryRight}\\| = \\|f\\|$$$

Lean4

@[simp]
theorem curryRight_norm (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖f.curryRight‖ = ‖f‖ :=
  (continuousMultilinearCurryRightEquiv 𝕜 Ei G).norm_map f

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