snd'

Mathlib.SetTheory.Ordinal.Notation

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

English

NF (oadd e n a) implies NFBelow a (repr e).

Русский

NF( oadd e n a ) => NFBelow a (repr e).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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