theorem Set.finset_subset_preimage_of_finite_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : (f '' s).Finite) : ∃ (s' : Finset α), ↑s' ⊆ s ∧ f '' ↑s' = f '' s ∧ s'.card = h.toFinset.card

Let $f: \alpha \to \beta$ be a function and $s \subseteq \alpha$ a subset with finite image $f(s)$. Then there exists a finite subset $s' \subseteq_{\text{fin}} s$ such that:

• $s' \subseteq s$ (subset relation)
• $f(s') = f(s)$ (image equality)
• $|s'| = |f(s)|$ (cardinality preservation)