quotientEquivClasses — Mathlib

English

There is a natural bijection between the quotient set α/r and the set of equivalence classes of r.

Русский

Существует естественная биекция между фактор-множество α/р и множеством классов эквивалентности r.

LaTeX

$$$\\\\operatorname{Quotient}(r) \\cong \\\\operatorname{Setoid.classes}(r)$$$

Lean4

/-- The equivalence between the quotient by an equivalence relation and its
type of equivalence classes. -/
noncomputable def quotientEquivClasses (r : Setoid α) : Quotient r ≃ Setoid.classes r :=
  by
  let f (a : α) : Setoid.classes r := ⟨{x | r x a}, Setoid.mem_classes r a⟩
  have f_respects_relation (a b : α) (a_rel_b : r a b) : f a = f b :=
    by
    rw [Subtype.mk.injEq]
    exact
      Setoid.eq_of_mem_classes (Setoid.mem_classes r a) (Setoid.symm a_rel_b) (Setoid.mem_classes r b) (Setoid.refl b)
  apply Equiv.ofBijective (Quot.lift f f_respects_relation)
  constructor
  · intro (q_a : Quotient r) (q_b : Quotient r) h_eq
    induction q_a using Quotient.ind with
    | _ a
    induction q_b using Quotient.ind with
    | _ b
    simp only [f, Quotient.lift_mk, Subtype.ext_iff] at h_eq
    apply Quotient.sound
    change a ∈ {x | r x b}
    rw [← h_eq]
    exact Setoid.refl a
  · rw [Quot.surjective_lift]
    intro ⟨c, a, hc⟩
    exact ⟨a, Subtype.ext hc.symm⟩

Похожие утверждения