Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 05:36 34f34942

View on Github →

chore(set_theory/cardinal): rename is_empty/nonempty lemmas (#9668)

  • add is_empty_pi, is_empty_prod, is_empty_pprod, is_empty_sum;
  • rename cardinal.eq_zero_of_is_empty to cardinal.mk_eq_zero, make the argument α : Type u explicit;
  • rename cardinal.eq_zero_iff_is_empty to cardinal.mk_eq_zero_iff;
  • rename cardinal.ne_zero_iff_nonempty to cardinal.mk_ne_zero_iff;
  • add @[simp] lemma cardinal.mk_ne_zero;
  • fix compile errors caused by these changes, golf a few proofs.

Estimated changes

added theorem is_empty_pi
added theorem is_empty_pprod
added theorem is_empty_prod
added theorem is_empty_psum
added theorem is_empty_sum
added theorem cardinal.mk_eq_zero
added theorem cardinal.mk_ne_zero
modified theorem cardinal.omega_ne_zero
modified theorem cardinal.prod_eq_zero