English
If a set maps into another finite set with an injective map, the domain is finite.
Русский
Если отображение сфере в конечное множество и инъективно на исходном множестве, то исходное множество конечно.
LaTeX
$$$\mathrm{MapsTo}(f,s,t) \land \mathrm{InjOn}(f,s) \land \mathrm{Finite}(t) \Rightarrow \mathrm{Finite}(s)$$$
Lean4
theorem of_injOn {f : α → β} {s : Set α} {t : Set β} (hm : MapsTo f s t) (hi : InjOn f s) (ht : t.Finite) : s.Finite :=
.of_finite_image (ht.subset (image_subset_iff.mpr hm)) hi