oadd_zero

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.NF.oadd_zero

English

If e is NF, then NF(oadd e n 0).

Русский

Если e имеет NF, то NF(oadd e n 0).

LaTeX

$$$NF(e) \Rightarrow NF(\mathrm{oadd}(e,n,0))$$$

Lean4

instance oadd_zero (e n) [h : NF e] : NF (ONote.oadd e n 0) :=
  h.oadd _ NFBelow.zero

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

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

Разделы

Аффилиация

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