Theorems · Theorem · order theory
Set.infinite_range_of_injective
∀ {α : Type u} {β : Type v} [Infinite α] {f : α → β}, Function.Injective f → (Set.range f).Infinite- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Infinite
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.
- Setproof · cited by 53,352
- Set.rangestatement · cited by 4,705
- Infinitestatement and proof · cited by 352
- Set.image_univproof · cited by 322
- Function.Injective.injOnproof · cited by 280
- Set.Infinitestatement and proof · cited by 263
- Set.infinite_univproof · cited by 13
- Set.infinite_image_iffproof · cited by 7
Cited by9
Results whose statement or proof uses this declaration.
- BddBelow.wellFoundedOn_ltproof · cited by 3
- Set.infinite_of_injective_forall_memproof · cited by 2
- wellQuasiOrderedLE_iffproof · cited by 1
- exists_infinite_discreteTopologyproof · cited by 0
- Set.Infinite.exists_subset_countable_infiniteproof · cited by 0
- Set.partiallyWellOrderedOn_iff_finite_antichainsproof · cited by 0
- infinite_range_add_nsmul_iffproof · cited by 0
- infinite_range_add_smul_iffproof · cited by 0
- IsSl2Triple.exists_hasPrimitiveVectorWithproof · cited by 0