curry_apply

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.curry_apply

English

For f: α × β →₀ M, and x ∈ α, y ∈ β, we have f.curry x y = f (x,y).

Русский

Для f: α×β →₀ M и элементов x ∈ α, y ∈ β выполняется f.curry x y = f(x,y).

LaTeX

$$$f.\text{curry}(x)(y) = f(x,y)$$$

Lean4

@[simp]
theorem curry_apply (f : α × β →₀ M) (x : α) (y : β) : f.curry x y = f (x, y) :=
  rfl

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

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

Разделы

Аффилиация

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