not_bddAbove — Mathlib

English

Let α be a preorder with a bottom element and locally finite order. If a subset s ⊆ α is infinite, then s has no upper bound; equivalently, s is not bounded above.

Русский

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

LaTeX

$$$\text{If } s \subseteq \alpha \text{ is infinite, then } \forall u \in \alpha, \exists x \in s: u < x.$$$

Lean4

theorem _root_.Set.Infinite.not_bddAbove {s : Set α} : s.Infinite → ¬BddAbove s :=
  mt BddAbove.finite

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