English
In a linear order, not bounded below is equivalent to: for every x there exists y ∈ s with y < x.
Русский
В линейном порядке не ограничено снизу эквивалентно: для каждого x существует y ∈ s, такой что y < x.
LaTeX
$$$\\\\lnot \\\\text{BddBelow}(s) \\\\iff \\\\forall x, \\\\exists y ∈ s, y < x$$$
Lean4
/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` that is less
than `x`. A version for preorders is called `not_bddBelow_iff'`. -/
theorem not_bddBelow_iff {α : Type*} [LinearOrder α] {s : Set α} : ¬BddBelow s ↔ ∀ x, ∃ y ∈ s, y < x :=
@not_bddAbove_iff αᵒᵈ _ _