Theorems · Theorem · combinatorics
Finset.mem_map
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β}, b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b- Defined in
- Mathlib.Data.Finset.Image
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.mapstatement · cited by 747
- Multiset.mem_mapproof · cited by 72
Cited by32
Results whose statement or proof uses this declaration.
- affineIndependent_iff_linearIndependent_vsubproof · cited by 11
- Finset.univ_map_equiv_to_embeddingproof · cited by 5
- Finset.mem_sigmaLiftproof · cited by 3
- cauchySeq_finset_iff_tsum_vanishingproof · cited by 3
- Matrix.frobenius_nnnorm_diagonalproof · cited by 2
- Set.Intersecting.disjoint_map_complproof · cited by 2
- Finset.mem_sumLift₂proof · cited by 2
- Finset.sum_comm'proof · cited by 2
- Finset.property_of_mem_map_subtypeproof · cited by 2
- Matrix.detp_mulproof · cited by 1
- UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbsproof · cited by 1
- Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_cardproof · cited by 1