transGen_wcovBy_eq_reflTransGen_covBy

English

The transitive closure of the weak cover relation equals the reflexive-transitive closure of the cover relation.

Русский

Переходное замыкание слабого покрытия равно рефлексивно-транзитивному замыканию покрытия.

LaTeX

$$$ \mathrm{TransGen}(\mathrm{WCovBy}) = \mathrm{ReflTransGen}(\mathrm{CovBy}) $$$

Lean4

theorem transGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    TransGen (· ⩿ · : α → α → Prop) = ReflTransGen (· ⋖ ·) := by rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]

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