piCurry_apply

Mathlib.Logic.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.piCurry_apply

English

The piCurry equivalence acts by converting a function of a pair into a curried function.

Русский

Эквивалентность piCurry преобразует функцию пары в карри-функцию.

LaTeX

$$$$ \\text{piCurry } \\gamma\\ f = \\Sigma.curry f. $$$$

Lean4

@[simp]
theorem piCurry_apply {α} {β : α → Type*} (γ : ∀ a, β a → Type*) (f : ∀ x : Σ i, β i, γ x.1 x.2) :
    piCurry γ f = Sigma.curry f :=
  rfl

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

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

Разделы

Аффилиация

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