not_bddAbove_iff_isCofinal — Mathlib

English

Let α be a linear order with no maximum element. Then a subset s ⊆ α is unbounded above if and only if it is cofinal in α.

Русский

Пусть α — линейный порядок без максимального элемента. Тогда множество s ⊆ α не ограничено сверху тогда и только тогда, когда оно кофинально в α.

LaTeX

$$$\\neg \\mathrm{BddAbove}(s) \\iff \\mathrm{IsCofinal}(s)$$

Lean4

/-- In a linear order with no maximum, cofinal sets are the same as unbounded sets. -/
theorem not_bddAbove_iff_isCofinal [NoMaxOrder α] {s : Set α} : ¬BddAbove s ↔ IsCofinal s :=
  not_iff_comm.1 not_isCofinal_iff_bddAbove

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