English
Let ι be a type with a linear order and a well-founded relation LT, and let β : ι → Type be a family of types such that each β i is a partially ordered set with a bottom and a top. Then the lexicographic order on the dependent function type ∀ i, β i is a bounded order.
Русский
Пусть ι — тип с линейным порядком и хорошо основанной связью LT, и пусть β : ι → Type — семейство типов так, что для каждого i множество β i частично упорядовано и имеет границы снизу и сверху. Тогда лексикографический порядок на зависимом произведении ∀ i, β i образует ограниченный порядок.
LaTeX
$$$(\text{LinearOrder } \iota) \land (\text{WellFoundedLT } \iota) \land (\forall a:\\iota,\ \PartialOrder (\beta a)) \land (\forall a:\\iota,\ BoundedOrder (\beta a)) \Rightarrow \text{BoundedOrder}(\mathrm{Lex}(\forall a:\\iota,\\beta a))$$$
Lean4
instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, BoundedOrder (β a)] :
BoundedOrder (Lex (∀ a, β a)) where
