English
If a Finset t is contained in the image f''s of a set s under f, then t is the image of some Finset s' contained in s.
Русский
Пусть Finset t ⊆ f''s, тогда существует Finset s' ⊆ s such that s'.image f = t.
LaTeX
$$$\\uparrow t \\subseteq f''s \\ \\Longrightarrow\\ \\exists s'\\; (\\uparrow s' \\subseteq s) \\wedge s'.image f = t$$$
Lean4
/-- If a `Finset` is a subset of the image of a `Set` under `f`,
then it is equal to the `Finset.image` of a `Finset` subset of that `Set`. -/
theorem subset_set_image_iff [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} :
↑t ⊆ f '' s ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ s'.image f = t :=
by
constructor
· intro h
letI : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
lift t to Finset s using h
refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
ext y; simp
· grind
