nonempty_Ioi_subtype — Mathlib

English

If α has no maximal element, then for any a, there exists x > a, so Ioi(a) is nonempty.

Русский

Если в порядке нет максимального элемента, то для любого a существует x > a, следовательно Ioi(a) непуст.

LaTeX

$$$ \operatorname{Nonempty}(\mathrm{Ioi}(a)) $$$

Lean4

/-- In an order without maximal elements, the intervals `Ioi` are nonempty. -/
instance nonempty_Ioi_subtype [NoMaxOrder α] : Nonempty (Ioi a) :=
  Nonempty.to_subtype nonempty_Ioi

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