unbounded_lt_Ioi — Mathlib

English

If α has a semilattice structure with no maximum, then the set Ioi(a) is unbounded with respect to the strict order <; i.e., for every b there is x ∈ Ioi(a) with b < x.

Русский

Если в α существует полулат, и нет максимального элемента, то Ioi(a) не ограничено сверху для строгого порядка <; для любого b существует x ∈ Ioi(a) с b < x.

LaTeX

$$$$\forall a \in \alpha,\ \forall b \in \alpha,\ \exists x \in Ioi(a)\ such\ that\ b < x.$$$$

Lean4

theorem unbounded_lt_Ioi [SemilatticeSup α] [NoMaxOrder α] (a : α) : Unbounded (· < ·) (Ioi a) :=
  unbounded_lt_of_unbounded_le (unbounded_le_Ioi a)

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