norm_uncurryMid — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem norm_uncurryMid (p : Fin (n + 1)) (f : Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i ↦ Ei (p.succAbove i)) G) :
    ‖f.uncurryMid p‖ = ‖f‖ :=
  (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).symm.norm_map f

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