English
If two functions f and g coincide on s (as sets), then their images of s are equal: image f s = image g s.
Русский
Если f и g совпадают на s (как на множестве), то их образы множества s совпадают: image f s = image g s.
LaTeX
$$$\\text{Set.EqOn } f g \; s \\Rightarrow \\operatorname{image}(f,s) = \\operatorname{image}(g,s)$$$
Lean4
theorem image_congr (h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s :=
by
ext
simp_rw [mem_image, ← bex_def]
exact exists₂_congr fun x hx => by rw [h hx]