English
Let r be a relation on a type α. Then the reflexive-transitive closure of the transitive closure of r equals the reflexive-transitive closure of r itself: ReflTransGen(TransGen r) = ReflTransGen r.
Русский
Пусть r — отношение на типе α. Тогда рефлексивно-транзитивное замыкание транспитивного замыкания r совпадает с рефлексивно-транзитивным замыканием самого r: ReflTransGen(TransGen r) = ReflTransGen r.
LaTeX
$$$\\\\operatorname{ReflTransGen}(\\\\operatorname{TransGen}(r)) = \\\\operatorname{ReflTransGen}(r)$$$
Lean4
@[simp]
theorem reflTransGen_transGen : ReflTransGen (TransGen r) = ReflTransGen r := by
simp only [← reflGen_transGen, transGen_idem]