Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.empty_of_not_nonempty

Modification history

2021-05-18 04:50

src/data/equiv/basic.lean

feat(logic/is_empty): Add is_empty typeclass (#7606) …

Deleted equiv.empty_of_not_nonempty View on Github →

2017-11-23 23:33

data/equiv.lean

feat(data/finset): fintype, multiset.sort, list.pmap

Added equiv.empty_of_not_nonempty View on Github →