curry_apply

Mathlib.Order.Hom.Basic

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

English

Applying curry to f returns a function that takes x and y to f(x,y).

Русский

Применение карри к f возвращает функцию, которая принимает x и y и равна f(x,y).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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