transGen_idem — Mathlib

English

TransGen composed with TransGen equals TransGen: TransGen (TransGen r) = TransGen r.

Русский

TransGen, композиция TransGen с TransGen равна TransGen: TransGen (TransGen r) = TransGen r.

LaTeX

$$$ \forall {α} {r : α \to α \to \mathrm{Prop}}, \mathrm{Eq} (\mathrm{Relation.TransGen} (\mathrm{Relation.TransGen} r)) (\mathrm{Relation.TransGen} r) $$$

Lean4

theorem transGen_idem : TransGen (TransGen r) = TransGen r :=
  transGen_eq_self transitive_transGen

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