Theorems · Theorem · combinatorics
Finset.eq_of_veq
∀ {α : Type u_1} {s t : Finset α}, s.val = t.val → s = t- Defined in
- Mathlib.Data.Finset.Defs
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Multisetstatement and proof · cited by 2,627
- Finset.valstatement and proof · cited by 438
- Multiset.Nodupproof · cited by 148
Cited by45
Results whose statement or proof uses this declaration.
- Finset.filter_congrproof · cited by 167
- Finset.map_eq_imageproof · cited by 50
- Finset.eq_of_subset_of_card_leproof · cited by 34
- Finset.erase_eq_of_notMemproof · cited by 30
- Finset.insert_eq_of_memproof · cited by 28
- Finset.map_mapproof · cited by 22
- Finset.image_imageproof · cited by 16
- Finset.disjiUnion_eq_biUnionproof · cited by 11
- Finset.filter_mapproof · cited by 9
- Finset.val_injectiveproof · cited by 9
- List.toFinset_consproof · cited by 8
- Finset.attach_image_valproof · cited by 6