Theorems · Theorem · combinatorics
Finset.map_eq_image
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α ↪ β) (s : Finset α), Finset.map f s = Finset.image (⇑f) s- Defined in
- Mathlib.Data.Finset.Image
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 74 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Function.Embeddingstatement and proof · cited by 988
- Finset.imagestatement · cited by 910
- Finset.mapstatement and proof · cited by 747
- Finset.eq_of_veqproof · cited by 45
- Finset.nodupproof · cited by 40
- Multiset.Nodup.dedupproof · cited by 15
Cited by50
Results whose statement or proof uses this declaration.
- Finset.map_valEmbedding_attachFinproof · cited by 10
- Finset.map_eraseproof · cited by 5
- Fin.univ_succproof · cited by 3
- four_functions_theoremproof · cited by 3
- SimpleGraph.cliqueSet_mapproof · cited by 3
- Finset.map_some_eraseNoneproof · cited by 3
- Fin.univ_succAboveproof · cited by 2
- Finset.image_add_left_Icoproof · cited by 2
- Finset.subset_map_iffproof · cited by 2
- Finset.map_subset_iff_subset_preimageproof · cited by 2
- Nat.image_div_divisors_eq_divisorsproof · cited by 2
- Fin.univ_castSuccEmbproof · cited by 1