English
For a nonempty s, s.Pairwise (f x = f y) iff there exists z with f x = z for all x ∈ s.
Русский
Для непустого s: попарность по тождественному relation на изображениях f x эквивалентна существованию общего z, такого что f x = z для всех x ∈ s.
LaTeX
$$${s : Set \alpha} \to (s.Nonempty) \Rightarrow (s.Pairwise (\lambda x y. f x = f y) \leftrightarrow \exists z, \forall x \in s, f x = z)$$$
Lean4
/-- For a nonempty set `s`, a function `f` takes pairwise equal values on `s` if and only if
for some `z` in the codomain, `f` takes value `z` on all `x ∈ s`. See also
`Set.pairwise_eq_iff_exists_eq` for a version that assumes `[Nonempty ι]` instead of
`Set.Nonempty s`. -/
theorem pairwise_eq_iff_exists_eq {s : Set α} (hs : s.Nonempty) {f : α → ι} :
(s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z :=
hs.pairwise_iff_exists_forall
