English
If α is a semilattice with a least upper bound structure and has no maximum element, then the tail Ioi(a) = { x ∈ α : a < x } is unbounded above with respect to ≤; i.e., for every b there exists x ∈ Ioi(a) with b ≤ x.
Русский
Пусть α имеет полное полуклассическое верхнее нижнее свойство и нет максимального элемента; тогда множество Ioi(a) = { x : a < x } не ограничено сверху по ≤; то есть для каждого b существует x ∈ Ioi(a) с b ≤ x.
LaTeX
$$$$\forall a \in \alpha,\ \forall b \in \alpha,\ \exists x \in Ioi(a)\ such\ that\ b \le x.$$$$
Lean4
theorem unbounded_le_Ioi [SemilatticeSup α] [NoMaxOrder α] (a : α) : Unbounded (· ≤ ·) (Ioi a) := fun b =>
let ⟨c, hc⟩ := exists_gt (a ⊔ b)
⟨c, le_sup_left.trans_lt hc, (le_sup_right.trans_lt hc).not_ge⟩
