English
If f: α → β is injective and β is finite, then α is finite.
Русский
Если f: α → β инъективно, и β конечно, то α тоже конечно.
LaTeX
$$$\text{Finite}(\beta) \land \text{Injective}(f) \Rightarrow \text{Finite}(\alpha)$$$
Lean4
/-- 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. -/
noncomputable def ofInjective [Fintype β] (f : α → β) (H : Function.Injective f) : Fintype α :=
letI := Classical.dec
if hα : Nonempty α then
letI := Classical.inhabited_of_nonempty hα
ofSurjective (invFun f) (invFun_surjective H)
else ⟨∅, fun x => (hα ⟨x⟩).elim⟩
