lt_iff_transGen_covBy — Mathlib

English

In a locally finite preorder, x < y holds iff there exists a finite CovBy chain from x to y.

Русский

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

LaTeX

$$$x < y \iff TransGen(\lambda p q => CovBy p q) x y$$$

Lean4

/-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/
theorem lt_iff_transGen_covBy [Preorder α] [LocallyFiniteOrder α] {x y : α} : x < y ↔ TransGen (· ⋖ ·) x y :=
  by
  refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩
  induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1

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