English
In a locally finite partial order, x ≤ y holds exactly when x is connected to y by a finite sequence of successive CovBy steps (reflTransGen of CovBy).
Русский
В локально конечном частично упорядоченном множестве x ≤ y тогда и только тогда, когда между x и y существует конечная последовательность шагов CovBy (замкнутость по отношению).
LaTeX
$$$x \le y \iff ReflTransGen( CovBy ) x y$$$
Lean4
theorem transGen_covBy_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) : TransGen (· ⋖ ·) x y := by
-- We proceed by well-founded induction on the cardinality of `Ico x y`.
-- It's impossible for the cardinality to be zero since `x < y`
-- `Ico x y` is a nonempty finset and so contains a maximal element `z` and
-- `Ico x z` has cardinality strictly less than the cardinality of `Ico x y`
obtain ⟨z, hxz, hz⟩ := (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 hxy
have z_card : #(Ico x z) < #(Ico x y) :=
card_lt_card <|
ssubset_iff_of_subset (Ico_subset_Ico_right hz.1.2.le) |>.mpr
⟨z, mem_Ico.2 hz.1, right_notMem_Ico⟩
/- Since `z` is maximal in `Ico x y`, `z ⋖ y`. -/
have hzy : z ⋖ y := ⟨hz.1.2, fun c hc hcy ↦ hc.not_ge <| hz.2 (⟨(hz.1.1.trans_lt hc).le, hcy⟩) hc.le⟩
by_cases hxz : x < z
· exact .tail (transGen_covBy_of_lt hxz) hzy
· simp only [lt_iff_le_not_ge, not_and, not_not] at hxz
exact .single (hzy.of_le_of_lt (hxz hz.1.1) hxy)
termination_by #(Ico x y)
