Commit 2023-01-13 16:42 c69248e3

View on Github →

feat port: Data.Multiset.Powerset (#1544)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Forall2.lean

modified theorem List.forall₂_eq_eq_eq

Created Mathlib/Data/Multiset/Powerset.lean

added theorem Multiset.bind_powerset_len

added theorem Multiset.card_powerset

added theorem Multiset.card_powersetLen

added theorem Multiset.map_single_le_powerset

added theorem Multiset.mem_powerset

added theorem Multiset.mem_powersetAux

added theorem Multiset.mem_powersetLen

added theorem Multiset.mem_powersetLenAux

added theorem Multiset.nodup_powerset

added theorem Multiset.pairwise_disjoint_powersetLen

added def Multiset.powerset

added def Multiset.powersetAux'

added theorem Multiset.powersetAux'_cons

added theorem Multiset.powersetAux'_nil

added def Multiset.powersetAux

added theorem Multiset.powersetAux_eq_map_coe

added theorem Multiset.powersetAux_perm

added theorem Multiset.powersetAux_perm_powersetAux'

added def Multiset.powersetLen

added def Multiset.powersetLenAux

added theorem Multiset.powersetLenAux_cons

added theorem Multiset.powersetLenAux_eq_map_coe

added theorem Multiset.powersetLenAux_nil

added theorem Multiset.powersetLenAux_perm

added theorem Multiset.powersetLenAux_zero

added theorem Multiset.powersetLen_card_add

added theorem Multiset.powersetLen_coe'

added theorem Multiset.powersetLen_coe

added theorem Multiset.powersetLen_cons

added theorem Multiset.powersetLen_empty

added theorem Multiset.powersetLen_le_powerset

added theorem Multiset.powersetLen_map

added theorem Multiset.powersetLen_mono

added theorem Multiset.powersetLen_zero_left

added theorem Multiset.powersetLen_zero_right

added theorem Multiset.powerset_aux'_perm

added theorem Multiset.powerset_coe'

added theorem Multiset.powerset_coe

added theorem Multiset.powerset_cons

added theorem Multiset.powerset_zero

added theorem Multiset.revzip_powersetAux'

added theorem Multiset.revzip_powersetAux

added theorem Multiset.revzip_powersetAux_lemma

added theorem Multiset.revzip_powersetAux_perm

added theorem Multiset.revzip_powersetAux_perm_aux'