le_iff_reflTransGen_covBy — Mathlib

English

In a locally finite preorder, x ≤ y holds iff there is a transitive chain from x to y using the covering relation.

Русский

В локально конечном предуровне x ≤ y эквивалентно существованию последовательности из покрытий от x до y.

LaTeX

$$$x \le y \iff TransGen(\lambda p q => p \mathrel{\mathrm{WCovBy}} q) x y$$$

Lean4

/-- In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`. -/
theorem le_iff_reflTransGen_covBy [PartialOrder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ ReflTransGen (· ⋖ ·) x y := by rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]

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