mathlib
a6b90beb - refactor(set_theory/cardinal/*): add `succ_order` instance, rename `succ` lemmas (#14244)

Commit
3 years ago
refactor(set_theory/cardinal/*): add `succ_order` instance, rename `succ` lemmas (#14244) We rename the lemmas on `cardinal.succ` to better match those from `succ_order`. - `succ_le` → `succ_le_iff` - `lt_succ` → `lt_succ_iff` - `lt_succ_self` → `lt_succ` We also add `succ_le_of_lt` and `le_of_lt_succ`.
Author
Parents
Loading