wcovBy_eq_reflGen_covBy — Mathlib

English

In any partial order, the weak cover relation is the reflexive-generated closure of the cover relation.

Русский

В произвольном частичном порядке слабое покрытие равно рефлексивному замыканию покрытия.

LaTeX

$$$ \mathrm{WCovBy}(x,y) \iff \mathrm{ReflGen}(\mathrm{CovBy})(x,y) $$$

Lean4

theorem wcovBy_eq_reflGen_covBy [PartialOrder α] : (· ⩿ · : α → α → Prop) = ReflGen (· ⋖ ·) := by ext x y;
  simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]

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