eqvGen_of_setoid — Mathlib

English

If r is already an equivalence relation, then its equivalence closure equals r.

Русский

Если r уже является отношением эквивалентности, то его эквивгенционная обертка равна r.

LaTeX

$$$$ EqvGen.setoid r.r = r. $$$$

Lean4

/-- The equivalence closure of an equivalence relation r is r. -/
@[simp]
theorem eqvGen_of_setoid (r : Setoid α) : EqvGen.setoid r.r = r :=
  le_antisymm (by rw [eqvGen_eq]; exact sInf_le fun _ _ => id) EqvGen.rel

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