Theorems · Theorem · combinatorics
Finset.attach_image_val
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, Finset.image Subtype.val s.attach = s- Defined in
- Mathlib.Data.Finset.Image
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.imagestatement · cited by 910
- Multiset.mapproof · cited by 876
- Finset.valproof · cited by 438
- Finset.attachstatement and proof · cited by 168
- Multiset.dedupproof · cited by 59
- Finset.eq_of_veqproof · cited by 45
- Multiset.attach_map_valproof · cited by 9
- Finset.image_valproof · cited by 5
- Finset.attach_valproof · cited by 2
- Finset.dedup_eq_selfproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- Finset.sum_attachproof · cited by 54
- Finset.prod_attachproof · cited by 22
- Finset.attach_affineCombination_coeproof · cited by 1
- Nat.divisors_eq_map_attach_Iic_factorization_prod_powproof · cited by 0
- Nat.properDivisors_eq_map_attach_Iio_factorization_prod_powproof · cited by 0
- Nat.Coprime.divisors_mulproof · cited by 0