Commit 2023-09-27 20:27 3ac819de

View on Github →

feat: Miscellaneous Finset lemmas (#7379)

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.erase_eq_iff_eq_insert

added theorem Finset.insert_erase_invOn

added theorem Finset.insert_sdiff_cancel

added theorem Finset.symmDiff_eq_empty

added theorem Finset.symmDiff_nonempty

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_sdiff_comm

Modified Mathlib/Data/Finset/Image.lean

added theorem Finset.image_inj

added theorem Finset.image_injective

added theorem Finset.image_ssubset_image

Modified Mathlib/Data/Finset/Slice.lean

deleted theorem Finset.Set.Sized.card_le

added theorem Set.Sized.card_le

added theorem Set.sized_empty

added theorem Set.sized_singleton