instOrderTopColexForallOfWellFoundedGT

English

If ι is linear and WellFoundedGT, and each β a has PartialOrder and OrderTop, then the Colex order on ∀ a, β a has an OrderTop.

Русский

Если ι линейно упорядочено и WellFoundedGT, и для каждого a β a имеет PartialOrder и OrderTop, то Colex-упорядочение на ∀ a, β a имеет верхнюю грань.

LaTeX

$$$ [LinearOrder ι] \\wedge [WellFoundedGT ι] \\wedge [\\forall a, PartialOrder (β a)] \\wedge [\\forall a, OrderTop (β a)] \\Rightarrow \\mathrm{OrderTop}(\\mathrm{Colex}(\\forall a, β a))$$$

Lean4

instance [LinearOrder ι] [WellFoundedGT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] : OrderTop (Colex (∀ a, β a))
    where
  top := toColex ⊤
  le_top _ := toColex_monotone le_top

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