English
If ι is linearly ordered and WellFoundedLT, and each β a has a PartialOrder and an OrderTop, then the Lex order on ∀ a, β a has an OrderTop; the top element is the Lex of the tops.
Русский
Если ι линейно упорядочено и имеется WellFoundedLT, и для каждого a β a имеет PartialOrder и OrderTop, то у Lex-порядка на ∀ a, β a существует верхняя граница; верхний элемент совпадает с Lex верхнего β a.
LaTeX
$$$ [LinearOrder ι] \\wedge [WellFoundedLT ι] \\wedge [\\forall a, PartialOrder (β a)] \\wedge [\\forall a, OrderTop (β a)] \\Rightarrow \\mathrm{OrderTop}(\\mathrm{Lex}(\\forall a, β a))$$$
Lean4
instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] : OrderTop (Lex (∀ a, β a))
where
top := toLex ⊤
le_top _ := toLex_monotone le_top
