Theorem Ordinal.add_le_of_limit

Modification history

2025-07-11 17:39
Mathlib/SetTheory/Ordinal/Arithmetic.lean
refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …
Deleted Ordinal.add_le_of_limitView on Github →
2025-03-18 10:08
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore(SetTheory): split `Ordinal/Arithmetic.lean` (#23017) …
Added Ordinal.add_le_of_limitView on Github →
2024-12-10 16:18
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat(SetTheory/Ordinal/Arithmetic): `a + b ≤ c ↔ ∀ d < b, a + d < c` (#19804)
Deleted Ordinal.add_le_of_limitView on Github →
2023-02-16 08:59
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: port SetTheory.Ordinal.Arithmetic (#2271)
Added Ordinal.add_le_of_limitView on Github →