oadd_pos

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.oadd_pos

English

The ordinal produced by oadd is positive: 0 < oadd e n a.

Русский

Условие: ноль меньше чем oadd e n a.

LaTeX

$$$0 < \operatorname{repr}(\mathrm{oadd}(e,n,a))$$$

Lean4

theorem oadd_pos (e n a) : 0 < oadd e n a :=
  @lt_of_lt_of_le _ _ _ (ω ^ repr e) _ (opow_pos (repr e) omega0_pos) (omega0_le_oadd e n a)

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

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

Разделы

Аффилиация

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