range_pairwise — Mathlib

English

If hr holds that r is pairwise on f, then the range of f is pairwise under r.

Русский

Если r попарно относительно f на всем домене, то образ f имеет попарность под r.

LaTeX

$$$ (\\text{Pairwise } (r\\text{ on } f)) \\Rightarrow (\\text{range } f).Pairwise r $$$

Lean4

theorem _root_.Pairwise.range_pairwise (hr : Pairwise (r on f)) : (Set.range f).Pairwise r :=
  image_univ ▸ (pairwise_univ.mpr hr).image

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