curryLeft_add

Mathlib.Analysis.NormedSpace.Alternating.Curry

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.curryLeft_add

English

Currying is additive: curryLeft(f+g) = curryLeft f + curryLeft g.

Русский

Каррирование сохраняет сложение: curryLeft(f+g) = curryLeft f + curryLeft g.

LaTeX

$$$curryLeft (f + g) = curryLeft f + curryLeft g$$$

Lean4

@[simp]
theorem curryLeft_add (f g : E [⋀^Fin (n + 1)]→L[𝕜] F) : curryLeft (f + g) = curryLeft f + curryLeft g :=
  rfl

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

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

Разделы

Аффилиация

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