curry_apply_succ

Mathlib.Data.Fin.Tuple.Curry

URI: https://scilib.ai/kg/mathlib#Function.FromTypes.curry_apply_succ

← MathLib Explorer

English

Uncurry and curry are inverses: uncurry (curry f) = f.

Русский

Раскаррирование и каррирование являются обратными: uncurry (curry f) = f.

LaTeX

$$$\\text{uncurry } (\\text{curry } f) = f$$$

Lean4

@[simp low]
theorem curry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (a : p 0) :
    curry f a = curry (f ∘ Fin.cons a) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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