noMaxOrder_of_nonempty — Mathlib

English

If ι has a preorder, α(i) has Preorder and NoMaxOrder, and every α(i) is nonempty, then Lex has NoMaxOrder.

Русский

Если ι имеет предорядок, α(i) имеет порядок и NoMaxOrder, и каждое α(i) непусто, то Lex имеет NoMaxOrder.

LaTeX

$$$\text{NoMaxOrder}(\Sigma_\text{Lex} i, α(i))$$$

Lean4

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

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