lt

Mathlib.SetTheory.Ordinal.Notation

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

English

If h: NFBelow (ONote.oadd e n a) b then repr e < b.

Русский

Если h: NFBelow(oadd e n a, b), то repr e < b.

LaTeX

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

Lean4

theorem lt {e n a b} (h : NFBelow (ONote.oadd e n a) b) : repr e < b := by obtain - | ⟨h₁, h₂, h₃⟩ := h; exact h₃

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

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

Разделы

Аффилиация

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