norm_curryMid — Mathlib

English

Alternative statement of norm preservation under index equivalence.

Русский

Альтернативная формулировка сохранения нормы при эквивалентности индексов.

LaTeX

$$$\\|\\mathrm{domDomCongr}\\;\\sigma\\;f\\| = \\|f\\|$$$

Lean4

@[simp]
theorem norm_curryMid (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G) : ‖f.curryMid p‖ = ‖f‖ :=
  (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).norm_map f

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