instOrderBotLexForallOfWellFoundedLT

English

Given a LinearOrder ι, WellFoundedLT ι, and β_i with PartialOrder, the Lex product over all i carries an OrderBot when each β_i has an OrderBot.

Русский

При линейном порядке ι и условии WellFoundedLT, если у каждого β_i есть OrderBot, то Lex-образование над всеми β_i имеет нижнюю границу.

LaTeX

$$$[LinearOrder ι] \\land [WellFoundedLT ι] \\land [\\forall i, PartialOrder (β i)] \\land [\\forall i, OrderBot (β i)] \\Rightarrow OrderBot(\\mathrm{Lex}((i:ι)\\to β i)).$$$

Lean4

instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] : OrderBot (Lex (∀ a, β a))
    where
  bot := toLex ⊥
  bot_le _ := toLex_monotone bot_le

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