Commit 2023-01-17 13:11 731a37cb

View on Github →

feat: port Data.Finset.Powerset (#1622)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Powerset.lean

added theorem Finset.card_powerset

added theorem Finset.card_powersetLen

added theorem Finset.coe_powerset

added def Finset.decidableExistsOfDecidableSsubsets'

added def Finset.decidableExistsOfDecidableSubsets'

added def Finset.decidableForallOfDecidableSsubsets'

added def Finset.decidableForallOfDecidableSubsets'

added theorem Finset.empty_mem_powerset

added theorem Finset.empty_mem_ssubsets

added theorem Finset.map_val_val_powersetLen

added theorem Finset.mem_powerset

added theorem Finset.mem_powersetLen

added theorem Finset.mem_powerset_self

added theorem Finset.mem_ssubsets

added theorem Finset.not_mem_of_mem_powerset_of_not_mem

added theorem Finset.pairwise_disjoint_powersetLen

added def Finset.powerset

added def Finset.powersetLen

added theorem Finset.powersetLen_card_add

added theorem Finset.powersetLen_empty

added theorem Finset.powersetLen_eq_filter

added theorem Finset.powersetLen_map

added theorem Finset.powersetLen_mono

added theorem Finset.powersetLen_nonempty

added theorem Finset.powersetLen_self

added theorem Finset.powersetLen_succ_insert

added theorem Finset.powersetLen_zero

added theorem Finset.powerset_card_bunionᵢ

added theorem Finset.powerset_card_disjUnionᵢ

added theorem Finset.powerset_empty

added theorem Finset.powerset_eq_singleton_empty

added theorem Finset.powerset_inj

added theorem Finset.powerset_injective

added theorem Finset.powerset_insert

added theorem Finset.powerset_len_sup

added theorem Finset.powerset_mono

added theorem Finset.powerset_nonempty

added def Finset.ssubsets