Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 15:43 9be82475

View on Github →

feat(logic/function/embedding): add function.embedding.option_elim (#9841)

  • add option.injective_iff;
  • add function.embedding.option_elim;
  • use it in the proof of cardinal.add_one_le_succ;
  • add function.embedding.cardinal_le, cardinal.succ_pos;
  • add @[simp] to cardinal.lt_succ.

Estimated changes

added theorem option.injective_iff
modified theorem cardinal.add_one_le_succ
modified theorem cardinal.lt_succ
modified theorem cardinal.succ_ne_zero
added theorem cardinal.succ_pos