instTransTransGen_mathlib — Mathlib

English

TransGen is idempotent under transitivity: composing TransGen with itself yields the same TransGen.

Русский

TransGen индуктивно тождественно относительно транспозиции: композиция TransGen с самим собой дает тот же TransGen.

LaTeX

$$$ \forall {α} {r : α \to α \to \mathrm{Prop}}, \mathrm{TransGen} (\mathrm{TransGen} r) = \mathrm{TransGen} r $$$

Lean4

instance : Trans (TransGen r) r (TransGen r) :=
  ⟨TransGen.tail⟩

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