Composite_of_Mapping_with_Inverse
Provedcomposite-mappingsequivalence-relationsinverse-mappingsproofwiki
Let f: S → T be a mapping. Then for all x in S, f⁻¹(f(x)) = [x]_{R_f}, the equivalence class of x under the equivalence induced by f.
Preamble
import Mathlib.Logic.Function.Basic import Mathlib.Data.Setoid.Basic
Formal statement
theorem Composite_of_Mapping_with_Inverse {α β : Type _} (f : α → β) (x y : α) (h : f x = f y) : Quotient.mk (Setoid.ker f) x = Quotient.mk (Setoid.ker f) y := by sorrySource