mathlib
34f34942 - chore(set_theory/cardinal): rename `is_empty`/`nonempty` lemmas (#9668)

Commit
4 years ago
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.
Author
Parents
Loading