not_bddAbove_iff — Mathlib

English

In a linear order, not bounded above is equivalent to: for every x there exists y ∈ s with x < y.

Русский

В линейном порядке не ограничено сверху эквивалентно: для каждого x существует y ∈ s, такой что x < y.

LaTeX

$$$\\\\lnot \\text{BddAbove}(s) \\\\iff \\\\forall x, \\\\exists y ∈ s, x < y$$$

Lean4

/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` that is greater
than `x`. A version for preorders is called `not_bddAbove_iff'`. -/
theorem not_bddAbove_iff {α : Type*} [LinearOrder α] {s : Set α} : ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, x < y := by
  simp only [not_bddAbove_iff', not_le]

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