le_iff_transGen_wcovBy — Mathlib

English

As above, there exists a finite chain from x to y with the covering relation when x ≤ y.

Русский

Как выше, существует конечная цепь от x до y с отношением покрытия при x ≤ y.

LaTeX

$$$x \le y \Rightarrow \operatorname{TransGen}(\lambda p q, p \mathrel{\mathrm{WCovBy}} q) x y$$$

Lean4

/-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/
theorem le_iff_transGen_wcovBy [Preorder α] [LocallyFiniteOrder α] {x y : α} : x ≤ y ↔ TransGen (· ⩿ ·) x y :=
  by
  refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩
  induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le

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