Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-05 20:54 1a45a56b

View on Github →

feat(logic/basic): subsingleton_of_not_nonempty (#7043) Also generalize not_nonempty_iff_imp_false to Sort *.

Estimated changes

modified theorem not_nonempty_iff_imp_false