English
If a Finset t is contained in the image s.image f of a Finset s under f, then t is the image of some Finset s' with s' ⊆ s.
Русский
Если Finset t ⊆ image f s, то существует Finset s' ⊆ s such that s'.image f = t.
LaTeX
$$$t \\subseteq s.image\, f \\iff \\exists s'\\; (s'\\subseteq s) \\land s'.image\, f = t$$$
Lean4
/-- If a finset `t` is a subset of the image of another finset `s` under `f`, then it is equal to the
image of a subset of `s`.
For the version where `s` is a set, see `subset_set_image_iff`.
-/
theorem subset_image_iff [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} :
t ⊆ s.image f ↔ ∃ s' : Finset α, s' ⊆ s ∧ s'.image f = t := by
simp only [← coe_subset, coe_image, subset_set_image_iff]
