Commit 2023-01-19 14:49 351f8682

View on Github →

feat: port Data.Fintype.Powerset (#1678)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Powerset.lean

added theorem Finset.mem_powerset_len_univ_iff

added theorem Finset.powerset_eq_univ

added theorem Finset.powerset_univ

added theorem Finset.univ_filter_card_eq

added theorem Fintype.card_finset

added theorem Fintype.card_finset_len

added theorem Fintype.card_set