English
For a nonempty s, the pairwise property of a function with respect to equality is equivalent to the existence of a common value.
Русский
Для непустого сета s попарная эквивалентность для функции по равенству эквивалентна существованию общего значения.
LaTeX
$$$tbd$$
Lean4
/-- A function `f : α → ι` with nonempty codomain takes pairwise equal values on a set `s` if and
only if for some `z` in the codomain, `f` takes value `z` on all `x ∈ s`. See also
`Set.Nonempty.pairwise_eq_iff_exists_eq` for a version that assumes `Set.Nonempty s` instead of
`[Nonempty ι]`. -/
theorem pairwise_eq_iff_exists_eq [Nonempty ι] (s : Set α) (f : α → ι) :
(s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z :=
pairwise_iff_exists_forall s f
