Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-12 13:05 73ccd02e

View on Github →

refactor(set_theory/cardinal): review API about #α = 2/nat.card α = 2 (#16899)

  • Rename cardinal.mk_eq_nat_iff_finset to cardinal.mk_set_eq_nat_iff_finset, add a version for types and cardinal.mk_eq_nat_iff_fintype.
  • Add cardinal.to_nat_eq_iff, a more general version of cardinal.to_nat_eq_one.
  • Rename cardinal.exists_not_mem_of_length_le to cardinal.exists_not_mem_of_length_lt.
  • Add cardinal.mk_eq_two_iff, cardinal.mk_eq_two_iff', nat.card_eq_two_iff, and nat.card_eq_two_iff'.

Estimated changes

added theorem cardinal.mk_eq_two_iff
added theorem cardinal.to_nat_eq_iff
modified theorem cardinal.two_le_iff'
added theorem nat.card_eq_two_iff'
added theorem nat.card_eq_two_iff