instNoMinOrderElemIio — Mathlib

English

If the ambient order has no minimal element, then the open interval Iio(a) has no minimal element as well.

Русский

Если в исходном порядке нет минимального элемента, то и в открытом интервале Iio(a) нет минимального элемента.

LaTeX

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

Lean4

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

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