English
In a locally finite preorder, if x ≤ y, then there exists a finite chain from x to y formed by successive covers.
Русский
В локально конечном предуровне существует конечная цепочка x = z0 ⩿ z1 ⩿ ... ⩿ zk = y, если x ≤ y.
LaTeX
$$$x \le y \Rightarrow \operatorname{TransGen}(\lambda p q, p \mathrel{\mathrm{WCovBy}} q) x y$$$
Lean4
theorem transGen_wcovBy_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) : TransGen (· ⩿ ·) x y := by
-- We proceed by well-founded induction on the cardinality of `Icc x y`.
-- It's impossible for the cardinality to be zero since `x ≤ y`
have : #(Ico x y) < #(Icc x y) :=
card_lt_card <| ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_notMem_Ico⟩⟩⟩
by_cases hxy' : y ≤ x
· exact .single <| wcovBy_of_le_of_le hxy hxy'
· obtain ⟨z, hxz, hz⟩ := (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'
have z_card :=
calc
#(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
_ < #(Icc x y) := this
have h₁ := transGen_wcovBy_of_le hz.1.1
have h₂ : z ⩿ y := ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
exact .tail h₁ h₂
termination_by #(Icc x y)
