snd

Mathlib.SetTheory.Ordinal.Notation

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

English

If NF(oadd e n a) then NF a.

Русский

Если NF(oadd e n a), тогда NF(a).

LaTeX

$$$NF(\mathrm{ONote.oadd}(e,n,a)) \Rightarrow NF(a)$$$

Lean4

theorem snd {e n a} (h : NF (oadd e n a)) : NF a :=
  ⟨⟨_, h.snd'⟩⟩

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

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

Разделы

Аффилиация

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