Quotient_Mapping_is_Surjection
Provedproofwikiquotient-mappingssurjections
Let R be an equivalence relation on S. Then the quotient mapping q_R: S → S/R is a surjection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Quotient_Mapping_is_Surjection {α : Type _} (s : Setoid α) : Function.Surjective (Quotient.mk s) := by sorrySource