English
If s surjects onto a Finset t via f, there exists a Finset u ⊆ s with f injective on u and u image f equals t.
Русский
Если s отображает на t через f_SURJ_ON, то существует подмножество u ⊆ s, на котором f инъективна и f(u)=t.
LaTeX
$$$ \forall s:\mathrm{Set}(\alpha),\ t:\mathrm{Finset}(\beta),\ hfs:\, s.SurjOn f t.toSet \Rightarrow \exists u:\mathrm{Finset}(\alpha), ↑u \subseteq s ∧ \operatorname{InjOn} f u ∧ f[u] = t $$$
Lean4
/-- `Finset` version of `Set.SurjOn.exists_subset_injOn_image_eq`. -/
theorem exists_subset_injOn_image_eq_of_surjOn [DecidableEq β] {f : α → β} (s : Set α) (t : Finset β)
(hfs : s.SurjOn f t) : ∃ u : Finset α, ↑u ⊆ s ∧ Set.InjOn f u ∧ u.image f = t :=
by
obtain ⟨u, hus, hf, himg⟩ := hfs.exists_subset_injOn_image_eq
refine ⟨(Finite.of_finite_image (by simp [himg]) hf).toFinset, by simpa, by simpa, ?_⟩
simpa [← Finset.coe_inj]
