noMinOrder_of_nonempty — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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