Theorems · Definition · combinatorics
Fintype.ofInjective
{α : Type u_1} → {β : Type u_2} → [Fintype β] → (f : α → β) → Function.Injective f → Fintype αGiven an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.
- Defined in
- Mathlib.Data.Fintype.OfMap
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
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.
- Fintypestatement and proof · cited by 7,736
- Function.invFunproof · cited by 60
- Function.invFun_surjectiveproof · cited by 8
- Fintype.ofSurjectiveproof · cited by 3
Cited by8
Results whose statement or proof uses this declaration.
- List.fixedLengthDigitsproof · cited by 13
- Nat.bijective_iff_injective_and_cardproof · cited by 3
- Set.surj_on_of_inj_on_of_ncard_leproof · cited by 1
- Fintype.sumRightproof · cited by 0
- SimpleGraph.nonempty_hom_of_forall_finite_subgraph_homproof · cited by 0
- DFunLike.fintypeproof · cited by 0
- Polynomial.fintypeSubtypeMonicDvdproof · cited by 0
- Fintype.sumLeftproof · cited by 0