unbounded_lt_inter_not_lt — Mathlib

English

For a semilattice with join, for every a, the set Ici(a) is unbounded with respect to the strict order <; i.e., there exist elements of Ici(a) arbitrarily large in the < order.

Русский

Для полусхождения с объединением для каждого a множество Ici(a) не ограничено сверху для строгого порядка <.

LaTeX

$$$$\forall a \in \alpha,\ \mathrm{Unbounded}_{<}(\mathrm{Ici}(a)).$$$$

Lean4

theorem unbounded_lt_inter_not_lt [SemilatticeSup α] (a : α) :
    Unbounded (· < ·) (s ∩ {b | ¬b < a}) ↔ Unbounded (· < ·) s :=
  by
  rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_lt_inter_not_lt a

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