Theorems · Theorem · combinatorics
Finset.univ_eq_attach
∀ {α : Type u} (s : Finset α), Finset.univ = s.attach- Defined in
- Mathlib.Data.Fintype.Sets
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.univstatement · cited by 3,473
- Finset.attachstatement · cited by 168
Cited by13
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.eq_infinitePiproof · cited by 6
- MeasureTheory.Measure.infinitePi_piproof · cited by 6
- Finset.prod_eq_prod_extendproof · cited by 3
- IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomicproof · cited by 3
- Equiv.Perm.OnCycleFactors.sign_kerParam_apply_applyproof · cited by 2
- SzemerediRegularity.card_incrementproof · cited by 2
- Finset.sum_attach_eq_sum_diteproof · cited by 1
- Finset.prod_attach_eq_prod_diteproof · cited by 1
- Finset.attach_affineCombination_coeproof · cited by 1
- Equiv.Perm.OnCycleFactors.kerParam_range_cardproof · cited by 1
- Finset.sum_eq_sum_extendproof · cited by 0
- Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_applyproof · cited by 0