reflTransGen_idem — Mathlib

English

The double application of TransGen yields the same as a single application: ReflTransGen(ReflTransGen r) = ReflTransGen r.

Русский

Двойное применение TransTransGen даёт то же, что и единичное: ReflTransGen(ReflTransGen r) = ReflTransGen r.

LaTeX

$$$$\\operatorname{ReflTransGen}(\\operatorname{ReflTransGen} r) = \\operatorname{ReflTransGen} r$$$$

Lean4

theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
  reflTransGen_eq_self reflexive_reflTransGen transitive_reflTransGen

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