English
The reflexive-transitive closure of the reflexive generator is equal to the reflexive-transitive closure.
Русский
Рефлексивно-транзитивное замыкание рефлексивного генератора равно рефлексивно-транзитивному замыканию.
LaTeX
$$$$\\operatorname{ReflTransGen}(\\operatorname{ReflGen} r) = \\operatorname{ReflTransGen} r$$$$
Lean4
@[simp]
theorem reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r := by
simp only [← transGen_reflGen, reflGen_eq_self reflexive_reflGen]