Theorems · Theorem · combinatorics
Finset.filter_map
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [inst : DecidablePred p],
Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)- Defined in
- Mathlib.Data.Finset.Image
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
- Assumes
- DecidablePred
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 and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Function.Embeddingstatement and proof · cited by 988
- Finset.filterstatement · cited by 949
- Finset.mapstatement · cited by 747
- Finset.valproof · cited by 438
- Finset.eq_of_veqproof · cited by 45
- Multiset.filter_mapproof · cited by 4
Cited by9
Results whose statement or proof uses this declaration.
- Finset.map_filterproof · cited by 2
- Finset.map_filter'proof · cited by 1
- MultilinearMap.domCoprod_alternizationproof · cited by 1
- MonoidHom.card_fiber_eq_of_mem_rangeproof · cited by 1
- Finset.map_truncatedInfproof · cited by 1
- Finset.map_truncatedSupproof · cited by 1
- Fin.card_filter_univ_succproof · cited by 1
- Finset.HasAntidiagonal.filter_snd_eq_antidiagonalproof · cited by 1
- AddMonoidHom.card_fiber_eq_of_mem_rangeproof · cited by 0