uncurry_apply_succ — Mathlib

English

Curry distributes over cons: curry f a equals curry (f ∘ Fin.cons a).

Русский

Кюрри распределяет над конструктором cons: curry f a = curry (f ∘ Fin.cons a).

LaTeX

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

Lean4

@[simp low]
theorem uncurry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : Function.FromTypes p τ)
    (args : (i : Fin (n + 1)) → p i) : uncurry f args = uncurry (f (args 0)) (Fin.tail args) :=
  rfl

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