instOrderBotColexForallOfWellFoundedGT

English

There is an order bottom on Colex(∀ a, β a), namely bot := toColex ⊥ with bot ≤ x for all x.

Русский

Существуют нижняя граница порядка на Colex(∀ a, β a), заданная bot := toColex ⊥, удовлетворяющая bot ≤ x для всех x в Colex(∀ a, β a).

LaTeX

$$$\text{bot} := \text{toColex}(\bot),\quad \text{bot} \le x\ \text{для всех } x \in \text{Colex}(\forall a, \beta a)$$$

Lean4

instance [LinearOrder ι] [WellFoundedGT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] : OrderBot (Colex (∀ a, β a))
    where
  bot := toColex ⊥
  bot_le _ := toColex_monotone bot_le

Похожие утверждения