uncurry_apply_cons — Mathlib

English

Uncurrying commutes with cons in the sense that uncurry f (Fin.cons a args) equals uncurry (f ∘' Fin.cons a) args.

Русский

Раскаррированный результат коммутирует с конструктором cons: uncurry f (Fin.cons a args) = uncurry (f ∘ Fin.cons a) args.

LaTeX

$$$\\text{uncurry } f (\\text{Fin.cons } a\\; args) = \\text{uncurry } (f \\circ' \\text{Fin.cons } a)\\; args$$$

Lean4

@[simp]
theorem uncurry_apply_cons {n : ℕ} {α} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes (vecCons α p) τ)
    (a : α) (args : (i : Fin n) → p i) : uncurry f (Fin.cons a args) = @uncurry _ p _ (f a) args :=
  rfl

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