conGen_idem — Mathlib

English

Applying conGen twice is the same as applying it once: conGen(conGen(r)) = conGen(r).

Русский

Повторное применение conGen даёт тот же результат: conGen(conGen(r)) = conGen(r).

LaTeX

$$$conGen(conGen(r)) = conGen(r)$$$

Lean4

/-- The map sending a binary relation to the smallest congruence relation in which it is
contained is idempotent. -/
@[to_additive addConGen_idem /-- The map sending a binary relation to the smallest additive
    congruence relation in which it is contained is idempotent. -/
    ]
theorem conGen_idem (r : M → M → Prop) : conGen (conGen r) = conGen r := by simp

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