curry_apply_cons

Mathlib.Data.Fin.Tuple.Curry

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

← MathLib Explorer

English

Curry for succ-case: curry f a equals curry (f ∘ Fin.cons a) for the successor encoding.

Русский

Кюрри для случая succ: curry f a = curry (f ∘ Fin.cons a).

LaTeX

$$$\\text{curry } f\\ a = \\text{curry } (f \\circ Fin.cons a)$$$

Lean4

@[simp]
theorem curry_apply_cons {n : ℕ} {α} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → (vecCons α p) i) → τ)
    (a : α) : curry f a = @curry _ p _ (f ∘' Fin.cons a) :=
  rfl

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

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

Разделы

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

Аффилиация

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