Theorems · Theorem · combinatorics
Finset.mem_powerset
∀ {α : Type u_1} {s t : Finset α}, s ∈ t.powerset ↔ s ⊆ t- Defined in
- Mathlib.Data.Finset.Powerset
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Multisetproof · cited by 2,627
- Finset.valproof · cited by 438
- Multiset.Nodupproof · cited by 148
- Finset.powersetstatement · cited by 93
- Multiset.powersetproof · cited by 27
- Finset.casesOnproof · cited by 17
- Finset.mk.injEqproof · cited by 4
Cited by26
Results whose statement or proof uses this declaration.
- Finset.powerset_card_disjiUnionproof · cited by 3
- Finset.powerset_monoproof · cited by 3
- summable_finsetProd_of_summable_nonnegproof · cited by 3
- Finset.sum_powerset_insertproof · cited by 2
- Finset.pluennecke_ruzsa_inequality_pow_div_pow_mulproof · cited by 2
- Finset.ruzsa_covering_addproof · cited by 2
- Finset.ruzsa_triangle_inequality_add_add_addproof · cited by 2
- Finset.ruzsa_triangle_inequality_mul_mul_mulproof · cited by 2
- Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_addproof · cited by 2
- Finset.sum_powerset_apply_cardproof · cited by 1
- Nat.smoothNumbersUpTo_subset_imageproof · cited by 1
- Finset.shatters_iffproof · cited by 1