Equivalence_Class_holds_Equivalent_Elements
Provedequivalence-classesproofwiki
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_Class_holds_Equivalent_Elements {α : Type _} (s : Setoid α) (x y : α) : s.r x y ↔ {z | s.r x z} = {z | s.r y z} := by sorrySource