Theorem Ordinal.add_le_iff

Modification history

2024-12-10 16:18
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat(SetTheory/Ordinal/Arithmetic): `a + b ≤ c ↔ ∀ d < b, a + d < c` (#19804)
Added Ordinal.add_le_iffView on Github →