Element_in_its_own_Equivalence_Class
Provedequivalence-classesfundamental-theorem-on-equivalence-relationsproofwiki
Let R be an equivalence relation on a set S. Then every element of S is in its own R-class.
Preamble
import Mathlib.Data.Setoid.Basic
Formal statement
theorem Element_in_its_own_Equivalence_Class {α : Type _} (s : Setoid α) (x : α) : x ∈ {y | s.r x y} := by sorrySource