Powerset

📁 Source: Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean

Statistics

Metric	Count
Definitions	0
Theorems prod_powerset, prod_powersetCard, prod_powerset_cons, prod_powerset_insert, sum_powerset, sum_powersetCard, sum_powerset_cons, sum_powerset_insert	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_powerset 📖	mathematical	—	prod Finset powerset range card powersetCard	—	Pairwise.set_pairwise pairwise_disjoint_powersetCard powerset_card_disjiUnion prod_disjiUnion
prod_powersetCard 📖	mathematical	—	prod Finset powersetCard card Monoid.toNatPow CommMonoid.toMonoid Nat.choose	—	prod_eq_pow_card mem_powersetCard card_powersetCard
prod_powerset_cons 📖	mathematical	Finset instMembership	prod powerset cons MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid attach notMem_mono instHasSubset mem_powerset	—	notMem_mono mem_powerset prod_congr cons_eq_insert prod_powerset_insert prod_attach
prod_powerset_insert 📖	mathematical	Finset instMembership	prod powerset instInsert MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	powerset_insert prod_union prod_image Set.InjOn.mono notMem_mono mem_powerset Set.LeftInvOn.injOn insert_erase_invOn
sum_powerset 📖	mathematical	—	sum Finset powerset range card powersetCard	—	Pairwise.set_pairwise pairwise_disjoint_powersetCard powerset_card_disjiUnion sum_disjiUnion
sum_powersetCard 📖	mathematical	—	sum Finset powersetCard card AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Nat.choose	—	sum_eq_card_nsmul mem_powersetCard card_powersetCard
sum_powerset_cons 📖	mathematical	Finset instMembership	sum powerset cons AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid attach notMem_mono instHasSubset mem_powerset	—	notMem_mono mem_powerset sum_congr cons_eq_insert sum_powerset_insert sum_attach
sum_powerset_insert 📖	mathematical	Finset instMembership	sum powerset instInsert AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	powerset_insert sum_union disjoint_left mem_powerset mem_image insert_subset_iff sum_image Set.InjOn.mono notMem_mono Set.LeftInvOn.injOn insert_erase_invOn

---

← Back to Index