lt_csSup_iff' — Mathlib

English

If s is bounded above, then a < sSup s iff there exists b ∈ s with a < b.

Русский

Если s ограничено сверху, то a < sSup s тогда и только тогда существует b ∈ s such that a < b.

LaTeX

$$$\text{BddAbove}(s) \Rightarrow a < sSup(s) \iff \exists b \in s, a < b$$$

Lean4

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_csSup_iff`. -/
theorem lt_csSup_iff' (hb : BddAbove s) : a < sSup s ↔ ∃ b ∈ s, a < b := by
  simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

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