uncurry_flip

Mathlib.Logic.Function.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem uncurry_flip {α β γ} (f : α → β → γ) : uncurry (flip f) = uncurry f ∘ Prod.swap :=
  rfl

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

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

Разделы

Аффилиация

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