omega0_le_oadd

Mathlib.SetTheory.Ordinal.Notation

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

← MathLib Explorer

English

For any e, n, a, we have ω^{repr(e)} ≤ repr(oadd e n a).

Русский

Для любых e, n, a выполняется ω^{repr(e)} ≤ repr(oadd(e,n,a)).

LaTeX

$$$\omega^{\operatorname{repr}(e)} \le \operatorname{repr}(\mathrm{oadd}(e,n,a))$$$

Lean4

theorem omega0_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a) :=
  by
  refine le_trans ?_ (le_add_right _ _)
  simpa using (mul_le_mul_iff_right₀ <| opow_pos (repr e) omega0_pos).2 (Nat.cast_le.2 n.2)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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