English
Every conditionally complete linear order with well-founded '<' can be turned into a successor order by defining succ(a) as the infimum of all larger elements, and proving the axioms of a successor order.
Русский
Каждый условно полноупорядоченный линейный порядок с хорошо упорядоченным '<' можно превратить в порядок-предшественник, задавая succ(a) какInf{ b > a } и доказывая аксиомы порядка-предшественника.
LaTeX
$$$ succ(a) = \\begin{cases} a, & \\text{если } \\mathrm{IsMax}(a) \\\\ \\inf\\{ b \\mid a < b \\}, & \\text{иначе} \\end{cases} \\,;\\text{ и это образует SuccOrder }\\alpha $$$
Lean4
/-- Every conditionally complete linear order with well-founded `<` is a successor order, by setting
the successor of an element to be the infimum of all larger elements. -/
noncomputable def toSuccOrder [WellFoundedLT α] : SuccOrder α
where
succ a := if IsMax a then a else sInf {b | a < b}
le_succ
a := by
by_cases h : IsMax a
· simp [h]
· simp only [h, ↓reduceIte]
rw [not_isMax_iff] at h
exact le_csInf h (fun b => le_of_lt)
max_of_succ_le
hs := by
by_contra h
simp [h] at hs
rw [not_isMax_iff] at h
exact hs.not_gt (csInf_mem h)
succ_le_of_lt {a b}
ha := by
simp only [ha.not_isMax, ↓reduceIte]
exact csInf_le ⟨a, fun _ hc => hc.le⟩ ha
