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