Theorems · Theorem · order theory
Set.card_range_of_injective
∀ {α : Type u} {β : Type v} [inst : Fintype α] {f : α → β},
Function.Injective f → ∀ [inst_1 : Fintype ↑(Set.range f)], Fintype.card ↑(Set.range f) = Fintype.card α- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Set.rangestatement and proof · cited by 4,705
- Fintype.cardstatement · cited by 1,386
- Fintype.card_congrproof · cited by 67
- Equiv.ofInjectiveproof · cited by 64
Cited by7
Results whose statement or proof uses this declaration.
- rank_eq_card_basisproof · cited by 8
- Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zeroproof · cited by 4
- Algebra.SubmersivePresentation.rank_kaehlerDifferentialproof · cited by 2
- EuclideanGeometry.exists_of_range_subset_orthocentricSystemproof · cited by 2
- Fintype.card_coeSort_rangeproof · cited by 1
- OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singletonproof · cited by 0
- Fintype.card_coeSort_mrangeproof · cited by 0