English
Let ι be a preorder and each α(i) be a preorder with no minimal element. Then the dependent lexicographic sigma-type Σₗ' i, α(i) also has no minimal element with respect to its natural order.
Русский
Пусть ι — множество с частично упорядоченным отношением, и для каждого i ∈ ι множество α(i) снабжено полным порядком без минимума. Тогда зависимый лексикографический сигма-тип Σₗ' i, α(i) также не имеет минимального элемента по своей естественной упорядоченности.
LaTeX
$$$$[\text{Preorder }\iota] \;[\forall i,\; \text{Preorder}(\alpha(i))] \;[\forall i,\; \text{NoMinOrder}(\alpha(i))] \Rightarrow \text{NoMinOrder}\Big(\Sigma_{\mathrm{Lex}}'_{i:\iota} \alpha(i)\Big).$$$$
Lean4
instance noMinOrder [Preorder ι] [∀ i, Preorder (α i)] [∀ i, NoMinOrder (α i)] : NoMinOrder (Σₗ' i, α i) :=
⟨by
rintro ⟨i, a⟩
obtain ⟨b, h⟩ := exists_lt a
exact ⟨⟨i, b⟩, right _ h⟩⟩
