noMaxOrder — Mathlib

English

Under similar hypotheses as above, the lexicographic sigma-type has no maximum.

Русский

При аналогичных гипотезах лексикографический сигма-тип не имеет максимального элемента.

LaTeX

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

Lean4

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

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