Theorems · Theorem · combinatorics
Set.toFinset_ofPred
∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype ↑{x | p x}],
{x | p x}.toFinset = Finset.filter p Finset.univ- Defined in
- Mathlib.Data.Fintype.Sets
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeDecidablePredFintype
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 · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Set.ofPredstatement and proof · cited by 6,101
- Finset.univstatement · cited by 3,473
- Finset.filterstatement · cited by 949
- Finset.extproof · cited by 565
- Set.toFinsetstatement · cited by 217
Cited by13
Results whose statement or proof uses this declaration.
- Set.Finite.toFinset_ofPredproof · cited by 3
- Fintype.prod_subtype_mul_prod_subtypeproof · cited by 2
- Fintype.sum_subtype_add_sum_subtypeproof · cited by 2
- alternatingGroup.coe_two_sylow_of_card_eq_fourproof · cited by 2
- FormalMultilinearSeries.leftInv_compproof · cited by 2
- FormalMultilinearSeries.comp_rightInv_aux1proof · cited by 2
- Group.nat_card_center_add_sum_card_noncenter_eq_cardproof · cited by 1
- SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_suppproof · cited by 1
- Set.card_ne_eqproof · cited by 1
- quadraticChar_card_sqrtsproof · cited by 1
- SimpleGraph.degree_eq_sum_if_adjproof · cited by 1
- SimpleGraph.Walk.IsEulerian.card_odd_degreeproof · cited by 0