norm_domDomCongr — Mathlib

English

For f on a sum of index sets, currySum m m' equals f on Sum.elim m m'.

Русский

Для f на сумме индексов, currySum m m' даёт f на Sum.elim m m'.

LaTeX

$$$f.currySum m m' = f (\\mathrm{Sum.elim}\\, m\, m')$$$

Lean4

@[simp]
theorem norm_domDomCongr (σ : ι ≃ ι') (f : ContinuousMultilinearMap 𝕜 (fun _ : ι => G) G') : ‖domDomCongr σ f‖ = ‖f‖ :=
  by
  simp only [norm_def, ← σ.prod_comp, (σ.arrowCongr (Equiv.refl G)).surjective.forall, domDomCongr_apply,
    Equiv.arrowCongr_apply, Equiv.coe_refl, comp_apply, Equiv.symm_apply_apply, id]

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