add_le_iff

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

If b ≠ 0, then a + b ≤ c iff for all d < b, a + d < c.

Русский

Если b ≠ 0, то a + b ≤ c эквивалентно для всех d < b выполнения a + d < c.

LaTeX

$$(b \neq 0) \Rightarrow (a + b \le c \iff \forall d < b, a + d < c)$$

Lean4

theorem add_le_iff {a b c : Ordinal} (hb : b ≠ 0) : a + b ≤ c ↔ ∀ d < b, a + d < c := by simpa using (lt_add_iff hb).not

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

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

Разделы

Аффилиация

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