instNoMinOrderLexForallOfWellFoundedLTOfNonempty

English

Let ι be a linearly ordered, nonempty index set with WellFoundedLT, and let β(i) be a type with a PartialOrder for every i, each having no minimal element. Then the lexicographic order on the Pi-type ∀ i, β(i) has no minimal element.

Русский

Пусть ι — ненулевой множество индексов с линейным порядком и WellFoundedLT, β(i) — множество с частичным порядком для каждого i, в каждом β(i) нет минимального элемента. Тогда лексикографический порядок на зависимости ∀ i, β(i) не имеет минимального элемента.

LaTeX

$$$\operatorname{NoMinOrder}\bigl(\operatorname{Lex}(\forall i\, \beta_i)\bigr)$$$

Lean4

instance [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [∀ i, PartialOrder (β i)] [∀ i, NoMinOrder (β i)] :
    NoMinOrder (Lex (∀ i, β i)) :=
  ⟨fun a =>
    let ⟨_, hb⟩ := exists_lt (ofLex a)
    ⟨_, toLex_strictMono hb⟩⟩

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