curry_apply

Mathlib.Topology.CompactOpen

URI: https://scilib.ai/kg/mathlib#ContinuousMap.curry_apply

English

For a curried f, applying to arguments a and b yields f(a,b).

Русский

Применяя закурированную форму к аргументам a и b, получаем f(a,b).

LaTeX

$$$f.curry\ a\ b = f(a,b)$$$

Lean4

@[simp]
theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) :=
  rfl

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

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

Разделы

Аффилиация

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