Theorem Cardinal.add_one_le_of_lt

Modification history

2026-04-18 06:23
Mathlib/SetTheory/Cardinal/Order.lean
chore(SetTheory/Cardinal): tweak `succ` lemmas (#36965) …
Added Cardinal.add_one_le_of_ltView on Github →