image — Mathlib

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

Похожие утверждения