reflGen_transGen — Mathlib

English

The reflexive generator of the transitive generator equals the reflexive-transitive closure.

Русский

Рефлексивный генератор TransGen равняется рефлексивно-транзитивному замыканию.

LaTeX

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

Lean4

@[simp]
theorem reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r :=
  by
  ext x y
  simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

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