English
If α and β have LocallyFiniteOrderTop structures, then their Lex sum α ⊕ₗ β carries a LocallyFiniteOrderTop structure, with explicit finite-interval correspondences for Ici and Ioi defined via disjoint sums and embeddings into Lex.
Русский
Если α и β обладают локально конечным верхним порядком, то их лексикографическая сумма α ⊕ₗ β также имеет локально конечный верхний порядок, причём интервалы Ici и Ioi задаются явно через разложение по частям и вложения в Lex.
LaTeX
$$$\\text{instLocallyFiniteOrderTop} \\; (\\alpha,\\beta) : \\text{LocallyFiniteOrderTop}(\\mathrm{Lex}(\\alpha,\\beta))$ with finsetIci := \\cdots, \\text{finsetIoi} := \\cdots$$$
Lean4
instance instLocallyFiniteOrderTop : LocallyFiniteOrderTop (α ⊕ₗ β)
where
finsetIci :=
Sum.elim (fun x => (Ici x).disjSum Finset.univ |>.map toLex.toEmbedding)
(Ici · |>.map (.trans .inr toLex.toEmbedding)) ∘
ofLex
finsetIoi :=
Sum.elim (fun x => (Ioi x).disjSum Finset.univ |>.map toLex.toEmbedding)
(Ioi · |>.map (.trans .inr toLex.toEmbedding)) ∘
ofLex
finset_mem_Ici := by simp
finset_mem_Ioi := by simp
