Commit 2023-12-26 22:33 401acd59

View on Github →

feat: Basic finset lemmas (#9225) From LeanAPAP and LeanCamCombi

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.Nonempty.exists_cons_eq

added theorem Finset.Nontrivial.exists_cons_eq

added theorem Finset.coe_subset_singleton

added theorem Finset.cons_sdiff_cons

added theorem Finset.disjoint_erase_insert

added theorem Finset.disjoint_insert_erase

added theorem Finset.erase_nonempty

added theorem Finset.erase_sdiff_erase

added theorem Finset.insert_sdiff_insert'

added theorem Finset.singleton_subset_coe

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Finset.filter_univ_mem

added theorem Finset.singleton_eq_univ

added theorem Finset.subset_compl_comm

added theorem Finset.subset_compl_singleton

Modified Mathlib/Data/Fintype/Card.lean

added theorem Fintype.card_additive

added theorem Fintype.card_multiplicative