Trivial_Quotient_is_a_Bijection
Provedbijectionsproofwikiquotient-sets
Let Δ_S be the diagonal relation on a set S. Then the quotient mapping q_{Δ_S}: S → S/Δ_S is a bijection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Trivial_Quotient_is_a_Bijection {α : Type _} : Function.Bijective (Quotient.mk (Setoid.mk (· = ·) ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩) : α → Quotient (Setoid.mk (· = ·) ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩)) := by sorrySource