English
If the image of s under f is finite and each fiber over an image point is finite when intersected with s, then s is finite.
Русский
Если образ s под действием f конечен и каждый ответвитель над точкой образа пересечение с s конечно, то s конечно.
LaTeX
$$$\\operatorname{Finite}(f(s)) \\rightarrow \\forall x \\in f(s), (s \\cap f^{-1} \\{x\\}).Finite \\rightarrow s\\Finite$$$
Lean4
/-- If the image of `s` under `f` is finite, and each fiber of `f` has a finite intersection
with `s`, then `s` is itself finite.
It is useful to give `f` explicitly here so this can be used with `apply`.
-/
theorem of_finite_fibers (f : α → β) {s : Set α} (himage : (f '' s).Finite)
(hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' { x }).Finite) : s.Finite :=
(himage.biUnion hfibers).subset fun x ↦ by aesop
