Commit 2025-06-07 13:26 3433dea2

View on Github →

feat(Finset/Card): relate cardinality of s \ t with t \ s (#25554) Add three iff lemmas which are often useful to compare cardinalities.

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Finset.card_sdiff_comm

added theorem Finset.card_sdiff_eq_card_sdiff_iff

added theorem Finset.card_sdiff_le_card_sdiff_iff

added theorem Finset.card_sdiff_lt_card_sdiff_iff