unbounded_lt_Ici — Mathlib

English

If α has a semilattice with no maximum, then Ici(a) is unbounded above with respect to the strict order <; 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 < x.$$$$

Lean4

theorem unbounded_lt_Ici [SemilatticeSup α] (a : α) : Unbounded (· < ·) (Ici a) := fun b =>
  ⟨a ⊔ b, le_sup_left, le_sup_right.not_gt⟩

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