English
A SuccOrder α can be built from a successor function with a relation to lt and le via an iff between a < b and succ a ≤ b; includes a max_of_succ_le property and succ_le_of_lt.
Русский
SuccOrder α строится из функции successor с отношениями lt и le через эквив между a < b и succ a ≤ b; включает свойства max_of_succ_le и succ_le_of_lt.
LaTeX
$$$\\text{SuccOrder}(\\alpha) = \\{ succ,\\ le\\_\\text{succ},\\ \\text{max_of_succ_le},\\ \\text{succ_le_of_lt} \\}$ так, что $a < b \\iff succ(a) \\le b$ (условие).$$
Lean4
/-- A well-order is a `SuccOrder`. -/
noncomputable def ofLinearWellFoundedLT [WellFoundedLT α] : SuccOrder α :=
ofCore (fun a ↦ if h : (Ioi a).Nonempty then wellFounded_lt.min _ h else a)
(fun ha _ ↦ by
rw [not_isMax_iff] at ha
simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]
exact ⟨(wellFounded_lt.min_le · ha), lt_of_lt_of_le (wellFounded_lt.min_mem _ ha)⟩)
fun _ ha ↦ dif_neg (not_not_intro ha <| not_isMax_iff.mpr ·)
