add_le_right_iff_mul_omega0_le

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.add_le_right_iff_mul_omega0_le

← MathLib Explorer

English

a + b ≤ b iff a · ω ≤ b.

Русский

a + b ≤ b эквивалентно a · ω ≤ b.

LaTeX

$$$$ a + b \le b \iff a \cdot \omega \le b $$$$

Lean4

theorem add_le_right_iff_mul_omega0_le {a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b :=
  by
  rw [← add_eq_right_iff_mul_omega0_le]
  exact (isNormal_add_right a).le_iff_eq

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

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

Разделы

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

Аффилиация

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