Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-20 18:26 a6b90beb

View on Github →

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.

Estimated changes

added theorem cardinal.le_of_lt_succ
added theorem cardinal.le_succ
modified theorem cardinal.lt_succ
added theorem cardinal.lt_succ_iff
deleted theorem cardinal.lt_succ_self
deleted theorem cardinal.succ_le
added theorem cardinal.succ_le_iff
added theorem cardinal.succ_le_of_lt
modified theorem cardinal.succ_nonempty
modified theorem cardinal.succ_pos