lt_ciSup_iff' — Mathlib

English

Let f : ι → α and a ∈ α with BddAbove (range f). Then a < iSup f iff ∃ i, a < f i.

Русский

Пусть f : ι → α и ⊤ ограниченность диапазона; тогда a < iSup f эквивалентно существованию i с a < f(i).

LaTeX

$$$ a < \inf_{i} f(i) \iff \exists i, a < f(i) $$$

Lean4

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_ciSup_iff`. -/
theorem lt_ciSup_iff' {f : ι → α} (h : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i := by
  simpa only [not_le, not_forall] using (ciSup_le_iff' h).not

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