Fundamental_Theorem_on_Equivalence_Relations
Provedequivalence-relationsfundamental-theorem-on-equivalence-relationsfundamental-theoremsproofwikiquotient-sets
Let R be an equivalence relation on a set S. Then the quotient S/R of S by R forms a partition of S.
Preamble
import Mathlib.Data.Setoid.Basic
Formal statement
theorem Fundamental_Theorem_on_Equivalence_Relations {α : Type _} [s : Setoid α] : ∀ a : Quotient s, ∃ x : α, Quotient.mk s x = a := by sorrySource