flip_curry

Mathlib.Logic.Function.Basic

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

English

For f: α × β → γ, flip (curry f) = curry (f ∘ Prod.swap).

Русский

Пусть f: α × β → γ. Тогда flip (curry f) = curry (f ∘ Prod.swap).

LaTeX

$$$ \\operatorname{flip}(\\operatorname{curry} f) = \\operatorname{curry}(f \\circ \\operatorname{Prod.swap}) $$$

Lean4

theorem flip_curry {α β γ} (f : α × β → γ) : flip (curry f) = curry (f ∘ Prod.swap) :=
  rfl

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

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

Разделы

Аффилиация

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