reflTransGen_wcovBy_eq_reflTransGen_covBy

English

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

Русский

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

LaTeX

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

Lean4

theorem reflTransGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    ReflTransGen (· ⩿ · : α → α → Prop) = ReflTransGen (· ⋖ ·) := by rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]

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