English
If s is pairwise with respect to r after applying f, then the image f''s is pairwise with respect to r.
Русский
Если множество s попарно относительно отношения r после применения функции f, то образ f[s] попарно относительно r.
LaTeX
$$$ s \\Pairwise ( r \\circ f ) \\Rightarrow ( f'' s ) \\Pairwise r $$$
Lean4
protected theorem image {s : Set ι} (h : s.Pairwise (r on f)) : (f '' s).Pairwise r :=
forall_mem_image.2 fun _x hx ↦ forall_mem_image.2 fun _y hy hne ↦ h hx hy <| ne_of_apply_ne _ hne