Composite_of_Quotient_Mappings
Provedequivalence-relationsproofwikiquotient-sets
Let R₁ be an equivalence on S, and R₂ be an equivalence on the quotient set S/R₁. Then there exists an equivalence R₃ on S such that (S/R₁)/R₂ is in bijection with S/R₃.
Preamble
import Mathlib.Logic.Equiv.Basic
Formal statement
theorem Composite_of_Quotient_Mappings {α : Type _} (s₁ : Setoid α) (s₂ : Setoid (Quotient s₁)) : ∃ s₃ : Setoid α, Nonempty (Quotient s₂ ≃ Quotient s₃) := by sorrySource