Theorems · Theorem · combinatorics
Finset.card_filter_le
∀ {α : Type u_1} (s : Finset α) (p : α → Prop) [inst : DecidablePred p], (Finset.filter p s).card ≤ s.card- Defined in
- Mathlib.Data.Finset.Card
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidablePred
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Finset.cardstatement · cited by 2,327
- Finset.filterstatement · cited by 949
- Finset.card_le_cardproof · cited by 118
- Finset.filter_subsetproof · cited by 55
Cited by16
Results whose statement or proof uses this declaration.
- PairReduction.exists_radius_leproof · cited by 4
- Nat.factorization_choose_le_logproof · cited by 3
- Rel.card_interedges_le_mulproof · cited by 2
- Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicityproof · cited by 2
- schnirelmannDensity_le_oneproof · cited by 2
- Finset.card_filter_eq_iffproof · cited by 2
- AddSubgroup.rank_closure_finset_le_cardproof · cited by 1
- Subgroup.rank_closure_finset_le_cardproof · cited by 1
- TwoUniqueProds.of_mulHomproof · cited by 1
- TwoUniqueSums.of_addHomproof · cited by 1
- MeasureTheory.Measure.haar.index_union_eqproof · cited by 1
- Finpartition.isUniform_oneproof · cited by 1