instNoMinOrderElemIic — Mathlib

English

If α has no minimal element, then the closed lower interval Iic(a) has no minimal element as well.

Русский

Если в порядке отсутствует минимальный элемент, то в замкнутом нижнем интервале Iic(a) тоже нет минимального элемента.

LaTeX

$$$ \operatorname{NoMinOrder}(\mathrm{Iic}(a)) $$$

Lean4

instance [NoMinOrder α] : NoMinOrder (Iic a) :=
  ⟨fun a =>
    let ⟨b, hb⟩ := exists_lt (a : α)
    ⟨⟨b, hb.le.trans a.2⟩, hb⟩⟩

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