reflTransGen_transGen — Mathlib

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]

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