English
Let s ⊆ ι be nonempty and r be an equivalence on α, with f : ι → α. Then s.Pairwise (r on f) iff there exists z ∈ α such that ∀ x ∈ s, r (f x) z.
Русский
Пусть s ⊆ ι непусто и r — эквивалентность на α, с f: ι → α. Тогда s.Pairwise (r on f) эквивалентно существованию z ∈ α такого, что ∀ x ∈ s, r (f x) z.
LaTeX
$$$[IsEquiv \alpha r] (s : Set ι) (hs : s.Nonempty) : s.Pairwise (r on f) \leftrightarrow \exists z, \forall x \in s, r (f x) z$$$
Lean4
theorem pairwise_iff_exists_forall [IsEquiv α r] {s : Set ι} (hs : s.Nonempty) :
s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z := by
constructor
· rcases hs with ⟨y, hy⟩
refine fun H => ⟨f y, fun x hx => ?_⟩
rcases eq_or_ne x y with (rfl | hne)
· apply IsRefl.refl
· exact H hx hy hne
· rintro ⟨z, hz⟩ x hx y hy _
exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (IsSymm.symm _ _ <| hz _ hy)
