noMinOrder_of_nonempty — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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