noMaxOrder_of_nonempty — Mathlib

English

If each α_i has no maximum, then the lexicographic sigma-type Σₗ' i, α_i has no maximum as well.

Русский

Если каждый α_i не имеет максимального элемента, то и у сигма-типа по лексикографическому порядку нет максимума.

LaTeX

$$$\\text{NoMaxOrder}(\\Sigma'_i,\\alpha_i)$$$

Lean4

instance noMaxOrder_of_nonempty [Preorder ι] [∀ i, Preorder (α i)] [NoMaxOrder ι] [∀ i, Nonempty (α i)] :
    NoMaxOrder (Σₗ' i, α i) :=
  ⟨by
    rintro ⟨i, a⟩
    obtain ⟨j, h⟩ := exists_gt i
    obtain ⟨b⟩ : Nonempty (α j) := inferInstance
    exact ⟨⟨j, b⟩, left _ _ h⟩⟩

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