English
Not bounded above is equivalent to: for every x there exists y in s with y not ≤ x.
Русский
Не ограничено сверху эквивалентно: для каждого x существует y ∈ s такое, что y > x.
LaTeX
$$$\\\\lnot \\text{BddAbove}(s) \\\\iff \\\\forall x, \\\\exists y \\in s, \\\\lnot y \\le x$$$
Lean4
/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` such that `x`
is not greater than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(y ≤ x)`. A version for linear orders is called `not_bddAbove_iff`. -/
theorem not_bddAbove_iff' : ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, ¬y ≤ x := by simp [BddAbove, upperBounds, Set.Nonempty]
