Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-05 00:55 a50170a8

View on Github →

chore(data/{finset,set}/basic): Align lemmas (#17805) Match the set and finset statements.

Estimated changes

added theorem finset.empty_ssubset
modified theorem set.compl_ne_univ
deleted theorem set.ne_empty_iff_nonempty
modified theorem set.nonempty.to_subtype
added theorem set.nonempty.to_type
modified theorem set.nonempty_compl
added theorem set.singleton_ne_empty