Equivalence_iff_Diagonal_and_Inverse_Composite
Provedequivalence-relationsproofwiki
Let R be an equivalence relation on S. Then R x y iff there exists z such that R x z and R y z (i.e., R = R ∘ R⁻¹).
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Equivalence_iff_Diagonal_and_Inverse_Composite {α : Type _} (R : α → α → Prop) (hRefl : ∀ x, R x x) (hSym : ∀ x y, R x y → R y x) (hTrans : ∀ x y z, R x y → R y z → R x z) : ∀ x y, R x y ↔ ∃ z, R x z ∧ R y z := by sorrySource