curry_uncurry

Mathlib.Data.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#Sigma.curry_uncurry

Lean4

@[simp]
theorem curry_uncurry {γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x), γ x y) : Sigma.curry (Sigma.uncurry f) = f :=
  rfl

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

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

Разделы

Аффилиация

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