mkClasses_classes — Mathlib

English

The equivalence relation built from the equivalence classes of an equivalence relation r is exactly r.

Русский

Эквивалентность, полученная из эквивалентных классов relation r, совпадает с самой r.

LaTeX

$$$\\mathrm{mkClasses}(r.classes,\\, \\mathrm{classes\\_eqv\\_classes}) = r.$$$

Lean4

/-- The equivalence relation made from the equivalence classes of an equivalence relation `r`
equals `r`. -/
theorem mkClasses_classes (r : Setoid α) : mkClasses r.classes classes_eqv_classes = r :=
  ext fun x _y =>
    ⟨fun h => r.symm' (h {z | r z x} (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
      eq_of_mem_classes (r.mem_classes x) (r.refl' x) hb hx ▸ r.symm' h⟩

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