Renaming_Mapping_is_Well_Defined
Provedequivalence-relationsmapping-theoryproofwikiquotient-sets
Let f: S → T be a mapping. The renaming mapping r: S/R_f → Im(f), defined as r([x]_{R_f}) = f(x) where R_f is the equivalence induced by f, is well-defined.
Preamble
import Mathlib.Logic.Function.Basic import Mathlib.Data.Setoid.Basic
Formal statement
theorem Renaming_Mapping_is_Well_Defined {α β : Type _} (f : α → β) : ∀ a b : α, f a = f b → Quotient.mk (Setoid.ker f) a = Quotient.mk (Setoid.ker f) b := by sorrySource