Theorems · Theorem · combinatorics
Finset.coe_image
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, ↑(Finset.image f s) = f '' ↑s- Defined in
- Mathlib.Data.Finset.Image
- Cited by
- 222 results in Mathlib
- Foundations
- Depth 76 from the axioms, rests on 1,372 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Set.imagestatement · cited by 5,609
- Set.extproof · cited by 2,266
- Finset.imagestatement · cited by 910
Cited by222
Results whose statement or proof uses this declaration.
- Module.Finite.of_basisproof · cited by 22
- Finset.coe_smul_finsetproof · cited by 16
- Finset.subset_set_image₂proof · cited by 10
- Module.Finite.of_isLocalizationproof · cited by 10
- AffineIndependent.finrank_vectorSpanproof · cited by 9
- Finset.coe_vadd_finsetproof · cited by 9
- Finset.image_image₂_distribproof · cited by 9
- LinearMap.trace_conj'proof · cited by 8
- Finset.image_preimageproof · cited by 8
- Finset.sum_of_injOnproof · cited by 8
- Algebra.EssFiniteType.compproof · cited by 7
- Ideal.FG.mapproof · cited by 7
Showing the 200 most cited of 222.