currySum_apply

Mathlib.Analysis.NormedSpace.Multilinear.Curry

URI: https://scilib.ai/kg/mathlib#ContinuousMultilinearMap.currySum_apply

← MathLib Explorer

English

Finalization: the norm under domDomCongr remains unchanged.

Русский

Окончательное утверждение: норма под domDomCongr не меняется.

LaTeX

$$$\\|domDomCongr σ f\\| = \\|f\\|$$$

Lean4

@[simp]
theorem currySum_apply (f : ContinuousMultilinearMap 𝕜 (fun _ : ι ⊕ ι' => G) G') (m : ι → G) (m' : ι' → G) :
    f.currySum m m' = f (Sum.elim m m') :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru