eqvGen_idem — Mathlib

English

Equivalence closure is idempotent: applying it twice gives the same result as applying it once.

Русский

Замыкание по эквивалентности идемпотентно: дважды применённое замыкание даёт то же, что и один раз.

LaTeX

$$$$ EqvGen.setoid (EqvGen.setoid r) = EqvGen.setoid r. $$$$

Lean4

/-- Equivalence closure is idempotent. -/
theorem eqvGen_idem (r : α → α → Prop) : EqvGen.setoid (EqvGen.setoid r) = EqvGen.setoid r :=
  eqvGen_of_setoid _

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