Powerset

📁 Source: Mathlib/Data/Multiset/Powerset.lean

Statistics

Metric	Count
Definitions powerset, powersetAux, powersetAux', powersetCard, powersetCardAux	5
Theorems ofPowerset, powerset, powersetCard, bind_powerset_len, card_powerset, card_powersetCard, map_single_le_powerset, mem_powerset, mem_powersetAux, mem_powersetCard, mem_powersetCardAux, nodup_powerset, pairwise_disjoint_powersetCard, powersetAux'_cons, powersetAux'_nil, powersetAux_eq_map_coe, powersetAux_perm, powersetAux_perm_powersetAux', powersetCardAux_cons, powersetCardAux_eq_map_coe, powersetCardAux_nil, powersetCardAux_perm, powersetCardAux_zero, powersetCard_card_add, powersetCard_coe, powersetCard_coe', powersetCard_cons, powersetCard_eq_empty, powersetCard_le_powerset, powersetCard_map, powersetCard_mono, powersetCard_one, powersetCard_zero_left, powersetCard_zero_right, powerset_aux'_perm, powerset_coe, powerset_coe', powerset_cons, powerset_eq_singleton_zero_iff, powerset_injective, powerset_le_powerset_iff_le, powerset_mono, powerset_strictMono, powerset_zero, revzip_powersetAux, revzip_powersetAux', revzip_powersetAux_lemma, revzip_powersetAux_perm, revzip_powersetAux_perm_aux', self_mem_powerset, zero_mem_powerset	51
Total	56

Multiset

Definitions

Name	Category	Theorems
powerset 📖	CompOp	22 math math: powerset_coe', zero_mem_powerset, antidiagonal_map_snd, mem_powerset, powerset_le_powerset_iff_le, sup_powerset_len, antidiagonal_eq_map_powerset, powerset_eq_singleton_zero_iff, powerset_zero, powerset_coe, nodup_powerset, map_single_le_powerset, antidiagonal_map_fst, Nodup.powerset, powerset_cons, card_powerset, powersetCard_le_powerset, powerset_injective, powerset_strictMono, bind_powerset_len, self_mem_powerset, powerset_mono
powersetAux 📖	CompOp	7 math math: powersetAux_perm_powersetAux', revzip_powersetAux_perm_aux', antidiagonal_coe, powersetAux_eq_map_coe, revzip_powersetAux_perm, powersetAux_perm, mem_powersetAux
powersetAux' 📖	CompOp	6 math math: powersetAux_perm_powersetAux', antidiagonal_coe', revzip_powersetAux_perm_aux', powersetAux'_nil, powersetAux'_cons, powerset_aux'_perm
powersetCard 📖	CompOp	19 math math: powersetCard_zero_left, IsNonarchimedean.multiset_powerset_image_add, powersetCard_zero_right, powersetCard_one, powersetCard_card_add, Finset.map_val_val_powersetCard, mem_powersetCard, sup_powerset_len, Nodup.powersetCard, powersetCard_coe, powersetCard_cons, card_powersetCard, powersetCard_mono, pairwise_disjoint_powersetCard, powersetCard_eq_empty, powersetCard_map, powersetCard_le_powerset, powersetCard_coe', bind_powerset_len
powersetCardAux 📖	CompOp	7 math math: powersetCardAux_eq_map_coe, mem_powersetCardAux, powersetCardAux_perm, powersetCard_coe', powersetCardAux_nil, powersetCardAux_zero, powersetCardAux_cons

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind_powerset_len 📖	mathematical	—	bind Multiset range card powersetCard powerset	—	powerset_coe' powersetCard_coe coe_bind coe_eq_coe List.range_bind_sublistsLen_perm
card_powerset 📖	mathematical	—	card Multiset powerset Monoid.toPow Nat.instMonoid	—	powerset_coe' List.length_sublists'
card_powersetCard 📖	mathematical	—	card Multiset powersetCard Nat.choose	—	powersetCard_coe List.length_sublistsLen
map_single_le_powerset 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder map instSingleton powerset	—	powerset_coe List.map_pure_sublist_sublists
mem_powerset 📖	mathematical	—	Multiset instMembership powerset Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	powerset_coe'
mem_powersetAux 📖	mathematical	—	Multiset powersetAux Preorder.toLE PartialOrder.toPreorder instPartialOrder ofList	—	—
mem_powersetCard 📖	mathematical	—	Multiset instMembership powersetCard Preorder.toLE PartialOrder.toPreorder instPartialOrder card	—	—
mem_powersetCardAux 📖	mathematical	—	Multiset powersetCardAux Preorder.toLE PartialOrder.toPreorder instPartialOrder ofList card	—	powersetCardAux_eq_map_coe
nodup_powerset 📖	mathematical	—	Nodup Multiset powerset	—	Nodup.of_map nodup_of_le map_single_le_powerset powerset_coe' List.Nodup.map_on List.mem_sublists' List.nodup_sublists'
pairwise_disjoint_powersetCard 📖	mathematical	—	Pairwise Disjoint Multiset instPartialOrder instOrderBot powersetCard	—	disjoint_left mem_powersetCard
powersetAux'_cons 📖	mathematical	—	powersetAux' Multiset cons	—	List.sublists'_cons
powersetAux'_nil 📖	mathematical	—	powersetAux' Multiset instZero	—	—
powersetAux_eq_map_coe 📖	mathematical	—	powersetAux Multiset ofList	—	—
powersetAux_perm 📖	mathematical	—	Multiset powersetAux	—	powersetAux_perm_powersetAux' powerset_aux'_perm
powersetAux_perm_powersetAux' 📖	mathematical	—	Multiset powersetAux powersetAux'	—	powersetAux_eq_map_coe List.sublists_perm_sublists'
powersetCardAux_cons 📖	mathematical	—	powersetCardAux Multiset cons	—	powersetCardAux_eq_map_coe List.sublistsLen_succ_cons
powersetCardAux_eq_map_coe 📖	mathematical	—	powersetCardAux Multiset ofList List.sublistsLen	—	powersetCardAux.eq_1 List.sublistsLenAux_eq
powersetCardAux_nil 📖	mathematical	—	powersetCardAux Multiset	—	—
powersetCardAux_perm 📖	mathematical	—	Multiset powersetCardAux	—	powersetCardAux_zero powersetCardAux_cons cons_swap
powersetCardAux_zero 📖	mathematical	—	powersetCardAux Multiset instZero	—	powersetCardAux_eq_map_coe List.sublistsLen_zero
powersetCard_card_add 📖	mathematical	—	powersetCard card Multiset instZero	—	powersetCard_eq_empty
powersetCard_coe 📖	mathematical	—	powersetCard ofList Multiset List.sublistsLen	—	powersetCardAux_eq_map_coe
powersetCard_coe' 📖	mathematical	—	powersetCard ofList Multiset powersetCardAux	—	—
powersetCard_cons 📖	mathematical	—	powersetCard cons Multiset instAdd map	—	powersetCardAux_cons
powersetCard_eq_empty 📖	mathematical	card	powersetCard Multiset instZero	—	card_eq_zero card_powersetCard Nat.choose_eq_zero_of_lt
powersetCard_le_powerset 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder powersetCard powerset	—	powersetCard_coe powerset_coe' List.sublistsLen_sublist_sublists'
powersetCard_map 📖	mathematical	—	powersetCard map Multiset	—	induction powersetCard_zero_left map_congr powersetCard_eq_empty map_cons powersetCard_cons map_map map_add
powersetCard_mono 📖	mathematical	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder powersetCard	—	leInductionOn powersetCard_coe List.sublistsLen_sublist_of_sublist
powersetCard_one 📖	mathematical	—	powersetCard map Multiset instSingleton	—	powersetCard_coe List.sublistsLen_one coe_reverse
powersetCard_zero_left 📖	mathematical	—	powersetCard Multiset instSingleton instZero	—	powersetCardAux_zero
powersetCard_zero_right 📖	mathematical	—	powersetCard Multiset instZero	—	—
powerset_aux'_perm 📖	mathematical	—	Multiset powersetAux'	—	powersetAux'_cons cons_swap
powerset_coe 📖	mathematical	—	powerset ofList Multiset	—	powersetAux_eq_map_coe
powerset_coe' 📖	mathematical	—	powerset ofList Multiset	—	powersetAux_perm_powersetAux'
powerset_cons 📖	mathematical	—	powerset cons Multiset instAdd map	—	powerset_coe' List.sublists'_cons map_congr
powerset_eq_singleton_zero_iff 📖	mathematical	—	powerset Multiset instSingleton instZero	—	card_powerset card_singleton Nat.instIsMulTorsionFree powerset_zero
powerset_injective 📖	mathematical	—	Multiset powerset	—	le_antisymm powerset_le_powerset_iff_le le_of_eq
powerset_le_powerset_iff_le 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder powerset	—	mem_powerset mem_of_le self_mem_powerset leInductionOn powerset_coe' coe_le List.Sublist.sublists'
powerset_mono 📖	mathematical	—	Monotone Multiset PartialOrder.toPreorder instPartialOrder powerset	—	StrictMono.monotone powerset_strictMono
powerset_strictMono 📖	mathematical	—	StrictMono Multiset PartialOrder.toPreorder instPartialOrder powerset	—	strictMono_of_le_iff_le powerset_le_powerset_iff_le
powerset_zero 📖	mathematical	—	powerset Multiset instZero instSingleton	—	—
revzip_powersetAux 📖	mathematical	Multiset powersetAux	Multiset instAdd ofList	—	List.revzip.eq_1 powersetAux_eq_map_coe List.revzip_sublists
revzip_powersetAux' 📖	mathematical	Multiset powersetAux'	Multiset instAdd ofList	—	List.revzip.eq_1 powersetAux'.eq_1 List.revzip_sublists'
revzip_powersetAux_lemma 📖	mathematical	Multiset instAdd ofList	Multiset instSub ofList	—	List.forall₂_map_right_iff List.forall₂_same add_tsub_cancel_left instOrderedSub instAddLeftReflectLE List.forall₂_eq_eq_eq List.revzip_map_fst
revzip_powersetAux_perm 📖	mathematical	—	Multiset powersetAux	—	revzip_powersetAux_lemma revzip_powersetAux coe_eq_coe powersetAux_perm
revzip_powersetAux_perm_aux' 📖	mathematical	—	Multiset powersetAux powersetAux'	—	revzip_powersetAux_lemma revzip_powersetAux revzip_powersetAux' powersetAux_perm_powersetAux'
self_mem_powerset 📖	mathematical	—	Multiset instMembership powerset	—	mem_powerset le_rfl
zero_mem_powerset 📖	mathematical	—	Multiset instMembership powerset instZero	—	mem_powerset zero_le

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofPowerset 📖	mathematical	Multiset.Nodup Multiset Multiset.powerset	Multiset.Nodup	—	Multiset.nodup_powerset
powerset 📖	mathematical	Multiset.Nodup	Multiset.Nodup Multiset Multiset.powerset	—	Multiset.nodup_powerset
powersetCard 📖	mathematical	Multiset.Nodup	Multiset.Nodup Multiset Multiset.powersetCard	—	Multiset.nodup_of_le Multiset.powersetCard_le_powerset Multiset.nodup_powerset

---

← Back to Index