Commit 2024-01-08 11:01 7445e724

View on Github →

feat: Basic finset lemmas (#9530) From LeanAPAP

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.cast_card_sdiff

Modified Mathlib/Data/Finset/Powerset.lean

modified theorem Finset.mem_powersetCard

modified theorem Finset.powersetCard_card_add

deleted theorem Finset.powersetCard_empty

added theorem Finset.powersetCard_empty_subsingleton

added theorem Finset.powersetCard_eq_empty

Modified Mathlib/Data/Fintype/Lattice.lean

added theorem Finset.mem_inf

Modified Mathlib/Data/Fintype/Powerset.lean

modified theorem Finset.mem_powersetCard_univ

Modified Mathlib/Data/Multiset/Powerset.lean

deleted theorem Multiset.powersetCard_empty

added theorem Multiset.powersetCard_eq_empty