English
If s is countable, and InjOn f (f^{-1} s), then the preimage f^{-1}(s) is countable.
Русский
Если s счетно, и InjOn f (f^{-1} s), то предобраз f^{-1}(s) счетен.
LaTeX
$$$\\operatorname{Countable}(s) \\Rightarrow \\exists f:\\ alpha\\to beta, \\operatorname{InjOn}(f, f^{-1}(s)) \\Rightarrow (f^{-1}(s)).Countable$$$
Lean4
theorem preimage_of_injOn {s : Set β} (hs : s.Countable) {f : α → β} (hf : InjOn f (f ⁻¹' s)) : (f ⁻¹' s).Countable :=
(mapsTo_preimage f s).countable_of_injOn hf hs