ofArity_succ

Mathlib.Logic.Function.OfArity

URI: https://scilib.ai/kg/mathlib#Function.ofArity_succ

English

OfArity α β (n+1) = α → OfArity α β n.

Русский

OfArity α β (n+1) = α → OfArity α β n.

LaTeX

$$$$\mathrm{OfArity}(\alpha,\beta, n.succ) = (\alpha \to \mathrm{OfArity}(\alpha,\beta,n)). $$$$

Lean4

@[simp]
theorem ofArity_succ (α β : Type u) (n : ℕ) : OfArity α β n.succ = (α → OfArity α β n) :=
  fromTypes_succ _ _

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

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

Разделы

Аффилиация

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