Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-22 23:07 3f164099

View on Github →

feat(data/finset/*): Random lemmas (#10955) Prove some compl lemmas for finset, (s.erase a).card + 1 = s.card for list, multiset, set, copy over one more generalized_boolean_algebra lemma.

Estimated changes

added theorem finset.map_nonempty
modified theorem finset.mem_sdiff
deleted theorem finset.nonempty.map
modified theorem finset.sdiff_ssubset
modified theorem finset.union_sdiff_symm
modified theorem finset.coe_compl
added theorem finset.compl_empty
modified theorem finset.compl_eq_univ_sdiff
added theorem finset.compl_erase
modified theorem finset.compl_filter
added theorem finset.compl_insert
modified theorem finset.compl_singleton
modified theorem finset.eq_univ_iff_forall
modified theorem finset.insert_compl_self
modified theorem finset.mem_compl
added theorem finset.not_mem_compl
modified theorem finset.union_compl