ofArity_zero

Mathlib.Logic.Function.OfArity

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

English

OfArity α β 0 is canonically equal to β.

Русский

OfArity α β 0 эквивалентно β.

LaTeX

$$$$\mathrm{OfArity}(\alpha,\beta,0) = \beta.$$$$

Lean4

@[simp]
theorem ofArity_zero (α β : Type u) : OfArity α β 0 = β :=
  fromTypes_zero _ _

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

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

Разделы

Аффилиация

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