instNoMinOrderColexForallOfWellFoundedGTOfNonempty

English

Let ι be a type with WellFoundedGT, Nonempty, and β(i) be partially ordered with NoMinOrder. Then the Colex order on the Pi-type ∀ i, β(i) has no minimal element.

Русский

Пусть ι имеет WellFoundedGT и не пусто; β(i) — частично упорядоченные множества без минимального элемента. Тогда Colex-упорядочение на ∀ i, β(i) не имеет минимального элемента.

LaTeX

$$$\operatorname{NoMinOrder}\bigl(\operatorname{Colex}(\forall i\, \beta_i)\bigr)$$$

Lean4

instance [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [∀ i, PartialOrder (β i)] [∀ i, NoMinOrder (β i)] :
    NoMinOrder (Colex (∀ i, β i)) :=
  inferInstanceAs (NoMinOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

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