Equivalence_Class_of_Element_is_Subset
Provedequivalence-classesproofwiki
Let R be an equivalence relation on a set S. The equivalence class of every element of S is a subset of S.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Equivalence_Class_of_Element_is_Subset {α : Type _} (r : α → α → Prop) (S : Set α) (hRefl : ∀ x ∈ S, r x x) (hSym : ∀ x y, r x y → r y x) (hS : ∀ x y, r x y → x ∈ S ∧ y ∈ S) (x : α) (hx : x ∈ S) : {y | r x y} ⊆ S := by sorrySource