curry_single — Mathlib

English

Curry of a singleton at (a,b) with value m equals a nested singleton: (single a (single b m)).curry = single a.1 (single a.2 m).

Русский

Каррирование одиночной функции на (a,b) со значением m равно вложенной одинокой функции: (single a (single b m)).curry = single a.1 (single a.2 m).

LaTeX

$$(\mathrm{single}\ (a,b)\ m).\text{curry} = \mathrm{single} (a.1) (\mathrm{single} (a.2) m)$$

Lean4

@[simp]
theorem curry_single (a : α × β) (m : M) : (single a m).curry = single a.1 (single a.2 m) := by
  rw [← curry_uncurry (single _ _), uncurry_single]

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