oadd

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.NFBelow.oadd

English

If e is NF and a is below repr e and repr e < b, then NFBelow(oadd e n a, b).

Русский

Если e имеет NF и a ниже repr(e) и repr(e) < b, то NFBelow(oadd e n a, b).

LaTeX

$$$NF(e) \land NFBelow(a, \operatorname{repr}(e)) \land \operatorname{repr}(e) < b \Rightarrow NFBelow(\mathrm{oadd}(e,n,a), b)$$$

Lean4

theorem oadd {e n a b} : NF e → NFBelow a (repr e) → repr e < b → NFBelow (oadd e n a) b
  | ⟨⟨_, h⟩⟩ => NFBelow.oadd' h

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

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

Разделы

Аффилиация

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