uncurry_apply_pair

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.uncurry_apply_pair

English

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

Русский

Для функции f: α →₀ β →₀ M и элементов a ∈ α, b ∈ β значение в паре (a,b) равно f(a)(b).

LaTeX

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

Lean4

@[simp]
protected theorem uncurry_apply_pair (f : α →₀ β →₀ M) (a : α) (b : β) : f.uncurry (a, b) = f a b :=
  rfl

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

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

Разделы

Аффилиация

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