uncurry_def

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.uncurry_def

English

The uncurry of a function f: α → β → γ is the function that maps a pair (a,b) to f a b.

Русский

Uncurry функции f: α → β → γ есть функция, сопоставляющая пару (a,b) выражение f a b.

LaTeX

$$$\operatorname{uncurry} f = \lambda p. f p.1 p.2$$$

Lean4

theorem uncurry_def {α β γ} (f : α → β → γ) : uncurry f = fun p ↦ f p.1 p.2 :=
  rfl

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

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

Разделы

Аффилиация

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