Equivalence_Classes_are_Disjoint
Provedequivalence-classesequivalence-classes-are-disjointfundamental-theorem-on-equivalence-relationsproofwiki
Let R be an equivalence relation on a set S. Then (x, y) ∉ R if and only if [x] ∩ [y] = ∅.
Preamble
import Mathlib.Data.Setoid.Basic import Mathlib.Data.Set.Basic
Formal statement
theorem Equivalence_Classes_are_Disjoint {α : Type _} (s : Setoid α) (x y : α) : ¬ s.r x y ↔ {z | s.r x z} ∩ {z | s.r y z} = ∅ := by sorrySource