English
The coercion of the image Finset to a Set equals the Set image of s to the image of f: ↑(image f s) = f '' ↑s.
Русский
Приведение образа Finset к множеству равно образу множества через f: ↑(image f s) = f '' ↑s.
LaTeX
$$$\\uparrow (\\operatorname{image}(f,s)) = f''\\uparrow s$$$
Lean4
@[simp, norm_cast]
theorem coe_image : ↑(s.image f) = f '' ↑s :=
Set.ext <| by simp only [mem_coe, mem_image, Set.mem_image, implies_true]