uncurry_apply — Mathlib

English

For any finitely supported function f: α →₀ β →₀ M and any pair (a,b), the value of the uncurry of f at (a,b) equals f(a)(b).

Русский

Для любой конечноподдерживаемой функции f: α →₀ β →₀ M и пары (a,b) значение раскаррирования f в точке (a,b) равно f(a)(b).

LaTeX

$$$(f.uncurry)(a,b) = f(a)(b)$$$

Lean4

protected theorem uncurry_apply (f : α →₀ β →₀ M) (x : α × β) : f.uncurry x = f x.1 x.2 :=
  rfl

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