const_zero

Mathlib.Logic.Function.OfArity

URI: https://scilib.ai/kg/mathlib#Function.OfArity.const_zero

English

@[simp] The constant 0-ary OfArity equals the codomain: OfArity α β 0 = β.

Русский

@[simp] константная 0-арная OfArity равна ядру β: OfArity α β 0 = β.

LaTeX

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

Lean4

@[simp]
theorem const_zero (α : Type u) {β : Type u} (b : β) : const α b 0 = b :=
  FromTypes.const_zero (fun _ => α) b

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

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

Разделы

Аффилиация

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