unbounded_le_Ici — Mathlib

English

If α is a semilattice with no maximum, then the closed tail Ici(a) = { x ∈ α : x ≥ a } is unbounded above with respect to ≤; i.e., for every b there exists x ∈ Ici(a) with b ≤ x.

Русский

Пусть α имеет полуклассическую упорядоченность без максимального элемента; тогда Ici(a) не ограничено сверху по ≤.

LaTeX

$$$$\forall a \in \alpha,\ \forall b \in \alpha,\ \exists x \in Ici(a)\ such\ that\ b \le x.$$$$

Lean4

theorem unbounded_le_Ici [SemilatticeSup α] [NoMaxOrder α] (a : α) : Unbounded (· ≤ ·) (Ici a) :=
  (unbounded_le_Ioi a).mono Set.Ioi_subset_Ici_self

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