Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-27 08:03 0c503262

View on Github →

refactor(*): use is_empty instead of not (nonempty α) (#8858) eq_empty_of_not_nonempty gets dropped in favour of eq_empty_of_is_empty.

Estimated changes

added theorem eq.not_gt
added theorem eq.not_lt
deleted theorem finset.univ_eq_empty'
modified theorem finset.univ_eq_empty
added theorem fintype.card_eq_zero
deleted theorem not_nonempty_fintype
added theorem measurable_const'
added theorem measurable_of_empty