Powerset

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

Statistics

Metric	Count
Definitions decidableExistsOfDecidableSSubsets, decidableExistsOfDecidableSSubsets', decidableExistsOfDecidableSubsets, decidableExistsOfDecidableSubsets', decidableForallOfDecidableSSubsets, decidableForallOfDecidableSSubsets', decidableForallOfDecidableSubsets, decidableForallOfDecidableSubsets', powerset, powersetCard, ssubsets	11
Theorems card_powerset, card_powersetCard, coe_powerset, empty_mem_powerset, empty_mem_ssubsets, image_injOn_powerset_of_injOn, image_surjOn_powerset, map_val_val_powersetCard, mem_powerset, mem_powersetCard, mem_powerset_self, mem_ssubsets, notMem_of_mem_powerset_of_notMem, pairwiseDisjoint_pair_insert, pairwise_disjoint_powersetCard, powersetCard_card_add, powersetCard_empty_subsingleton, powersetCard_eq_empty, powersetCard_eq_filter, powersetCard_map, powersetCard_mono, powersetCard_nonempty, powersetCard_nonempty_of_le, powersetCard_one, powersetCard_self, powersetCard_succ_insert, powersetCard_sup, powersetCard_zero, powerset_card_biUnion, powerset_card_disjiUnion, powerset_empty, powerset_eq_singleton_empty, powerset_image, powerset_inj, powerset_injective, powerset_insert, powerset_mono, powerset_nonempty	38
Total	49

Finset

Definitions

Name	Category	Theorems
decidableExistsOfDecidableSSubsets 📖	CompOp	—
decidableExistsOfDecidableSSubsets' 📖	CompOp	—
decidableExistsOfDecidableSubsets 📖	CompOp	—
decidableExistsOfDecidableSubsets' 📖	CompOp	—
decidableForallOfDecidableSSubsets 📖	CompOp	—
decidableForallOfDecidableSSubsets' 📖	CompOp	—
decidableForallOfDecidableSubsets 📖	CompOp	—
decidableForallOfDecidableSubsets' 📖	CompOp	—
powerset 📖	CompOp	60 math math: Nat.smoothNumbersUpTo_subset_image, powerset_eq_singleton_empty, Icc_eq_image_powerset, prod_add, powerset_insert, inclusion_exclusion_card_inf_compl, coe_powerset, Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers, prod_sub, image_surjOn_powerset, powerset_sups_powerset_self, powerset_infs_powerset_self, ContinuousMultilinearMap.map_piecewise_add, powerset_card_biUnion, inclusion_exclusion_sum_inf_compl, powerset_inj, powersetCard_eq_filter, Filter.tendsto_finset_powerset_atTop_atTop, prod_one_add, powerset_image, mem_powerset, inclusion_exclusion_card_biUnion, MeasureTheory.integral_biUnion_eq_sum_powerset, powerset_nonempty, Iic_eq_powerset, Nat.sum_divisors_filter_squarefree, image_injOn_powerset_of_injOn, powerset_injective, empty_mem_powerset, MultilinearMap.map_piecewise_add, sum_powerset_neg_one_pow_card_of_nonempty, sum_pow_mul_eq_add_pow, sum_powerset_insert, prod_powerset, sum_powerset, powerset_inter, prod_powerset_cons, filter_subset_univ, inclusion_exclusion_sum_biUnion, ContinuousAlternatingMap.map_piecewise_add, shatters_iff, powerset_card_disjiUnion, Ioc_eq_filter_powerset, powerset_empty, sum_powerset_neg_one_pow_card, powerset_mono, sum_powerset_apply_card, powerset_union, Nat.divisors_filter_squarefree, MeasureTheory.measureReal_biUnion_eq_sum_powerset, sum_powerset_cons, indicator_biUnion_eq_sum_powerset, powerset_univ, pairwiseDisjoint_pair_insert, mem_powerset_self, prod_powerset_insert, Icc_eq_filter_powerset, prod_add_one, card_powerset, powerset_eq_univ
powersetCard 📖	CompOp	39 math math: Lagrange.eval_iterate_derivative_eq_sum, map_val_val_powersetCard, powersetCard_mono, prod_powersetCard, Set.Sized.subset_powersetCard_univ, powersetCard_card_add, powerset_card_biUnion, subset_powersetCard_univ_iff, powersetCard_map, powersetCard_eq_filter, prod_X_add_C_coeff, Set.powersetCard.coe_finset, Lagrange.iterate_derivative_interpolate, MvPolynomial.support_esymm', mem_powersetCard, Polynomial.iterate_derivative_prod_X_sub_C, prod_powerset, sum_powerset, mem_powersetCard_univ, powersetCard_sup, MvPolynomial.esymm_eq_sum_monomial, powersetCard_nonempty, esymm_map_val, powersetCard_zero, MvPolynomial.support_esymm'', powerset_card_disjiUnion, card_powersetCard, sum_powersetCard, IsNonarchimedean.finset_powerset_image_add, powersetCard_eq_empty, MvPolynomial.support_esymm, powersetCard_succ_insert, powersetCard_one, univ_filter_card_eq, Set.sized_powersetCard, powersetCard_nonempty_of_le, pairwise_disjoint_powersetCard, powersetCard_empty_subsingleton, powersetCard_self
ssubsets 📖	CompOp	6 math math: Ioo_eq_filter_ssubsets, Ico_eq_filter_ssubsets, Ico_eq_image_ssubsets, mem_ssubsets, empty_mem_ssubsets, Iio_eq_ssubsets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_powerset 📖	mathematical	—	card Finset powerset Monoid.toNatPow Nat.instMonoid	—	Multiset.card_pmap Multiset.card_powerset
card_powersetCard 📖	mathematical	—	card Finset powersetCard Nat.choose	—	Multiset.card_pmap Multiset.card_powersetCard
coe_powerset 📖	mathematical	—	SetLike.coe Finset instSetLike powerset Set.preimage Set Set.powerset	—	Set.ext instIsConcreteLE
empty_mem_powerset 📖	mathematical	—	Finset instMembership powerset instEmptyCollection	—	—
empty_mem_ssubsets 📖	mathematical	Nonempty	Finset instMembership ssubsets instEmptyCollection	—	mem_ssubsets ssubset_iff_subset_ne empty_subset Nonempty.ne_empty
image_injOn_powerset_of_injOn 📖	mathematical	Set.InjOn SetLike.coe Finset instSetLike	image powerset	—	—
image_surjOn_powerset 📖	mathematical	—	Set.SurjOn Finset image SetLike.coe instSetLike powerset	—	—
map_val_val_powersetCard 📖	mathematical	—	Multiset.map Finset Multiset val powersetCard Multiset.powersetCard	—	Multiset.map_pmap Multiset.pmap_eq_map Multiset.map_id'
mem_powerset 📖	mathematical	—	Finset instMembership powerset instHasSubset	—	—
mem_powersetCard 📖	mathematical	—	Finset instMembership powersetCard instHasSubset card	—	val_le_iff
mem_powerset_self 📖	mathematical	—	Finset instMembership powerset	—	instReflSubset
mem_ssubsets 📖	mathematical	—	Finset instMembership ssubsets instHasSSubset	—	ssubsets.eq_1 mem_erase mem_powerset ssubset_iff_subset_ne
notMem_of_mem_powerset_of_notMem 📖	—	Finset instMembership powerset	—	—	mem_powerset
pairwiseDisjoint_pair_insert 📖	mathematical	Finset instMembership	Set.PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe instSetLike powerset Set.instInsert Set.instSingletonSet instInsert	—	notMem_mono mem_insert_self Set.LeftInvOn.injOn insert_erase_invOn
pairwise_disjoint_powersetCard 📖	mathematical	—	Pairwise Disjoint Finset partialOrder instOrderBot powersetCard	—	disjoint_left mem_powersetCard
powersetCard_card_add 📖	mathematical	—	powersetCard card Finset instEmptyCollection	—	—
powersetCard_empty_subsingleton 📖	mathematical	—	Set.Subsingleton Finset SetLike.coe instSetLike powersetCard instEmptyCollection	—	—
powersetCard_eq_empty 📖	mathematical	—	powersetCard Finset instEmptyCollection card	—	Mathlib.Tactic.Contrapose.contrapose₁ exists_subset_card_eq card_eq_zero card_powersetCard Nat.choose_eq_zero_of_lt
powersetCard_eq_filter 📖	mathematical	—	powersetCard filter Finset card powerset	—	ext
powersetCard_map 📖	mathematical	—	powersetCard map Finset RelEmbedding.toEmbedding Preorder.toLE PartialOrder.toPreorder partialOrder mapEmbedding	—	ext card_map
powersetCard_mono 📖	mathematical	Finset instHasSubset	powersetCard	—	mem_powersetCard Subset.trans
powersetCard_nonempty 📖	mathematical	—	Nonempty Finset powersetCard card	—	—
powersetCard_nonempty_of_le 📖	mathematical	card	Nonempty Finset powersetCard	—	powersetCard_nonempty
powersetCard_one 📖	mathematical	—	powersetCard map Finset instSingleton singleton_injective	—	eq_of_veq singleton_injective Multiset.map_injective val_injective map_val_val_powersetCard Multiset.powersetCard_one Multiset.map_congr Multiset.map_map
powersetCard_self 📖	mathematical	—	powersetCard card Finset instSingleton	—	ext mem_powersetCard mem_singleton eq_of_subset_of_card_le Eq.ge instReflSubset
powersetCard_succ_insert 📖	mathematical	Finset instMembership	powersetCard instInsert instUnion decidableEq image	—	powersetCard_eq_filter powerset_insert filter_union
powersetCard_sup 📖	mathematical	card	sup Finset Lattice.toSemilatticeSup instLattice instOrderBot powersetCard	—	le_antisymm sup_eq_biUnion le_iff_subset subset_iff powersetCard_nonempty le_trans pred_card_le_card_erase insert_erase powersetCard_succ_insert notMem_erase mem_union_right mem_image_of_mem mem_insert_self
powersetCard_zero 📖	mathematical	—	powersetCard Finset instSingleton instEmptyCollection	—	—
powerset_card_biUnion 📖	mathematical	—	powerset biUnion Finset range card powersetCard	—	Pairwise.set_pairwise pairwise_disjoint_powersetCard disjiUnion_eq_biUnion powerset_card_disjiUnion
powerset_card_disjiUnion 📖	mathematical	—	powerset disjiUnion Finset range card powersetCard Pairwise.set_pairwise Disjoint partialOrder instOrderBot pairwise_disjoint_powersetCard SetLike.coe instSetLike	—	ext Pairwise.set_pairwise pairwise_disjoint_powersetCard mem_disjiUnion mem_range card_le_card mem_powerset mem_powersetCard
powerset_empty 📖	mathematical	—	powerset Finset instEmptyCollection instSingleton	—	—
powerset_eq_singleton_empty 📖	mathematical	—	powerset Finset instSingleton instEmptyCollection	—	powerset_empty
powerset_image 📖	mathematical	—	powerset image Finset decidableEq	—	ext mem_image
powerset_inj 📖	mathematical	—	powerset	—	powerset_injective
powerset_injective 📖	mathematical	—	Finset powerset	—	Function.Injective.of_eq_imp_le powerset_mono Eq.le
powerset_insert 📖	mathematical	—	powerset Finset instInsert instUnion decidableEq image	—	ext
powerset_mono 📖	mathematical	—	Finset instHasSubset powerset	—	mem_powerset mem_powerset_self Subset.trans
powerset_nonempty 📖	mathematical	—	Nonempty Finset powerset	—	empty_mem_powerset

---

← Back to Index