reflTransGen_reflGen — Mathlib

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]

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