exists_lt_of_lt_ciSup — Mathlib

English

Indexed version of exists_lt_of_lt_csSup: if b < iSup f, there exists i with b < f(i).

Русский

Индексированная версия существования: если b меньше верхней грани iSup f, то существует i, для которого b < f(i).

LaTeX

$$$\text{If } b < i\!\text{Sup} f, \text{ then } \exists i, b < f(i).$$$

Lean4

/-- Indexed version of `exists_lt_of_lt_csSup`.
When `b < iSup f`, there is an element `i` such that `b < f i`.
-/
theorem exists_lt_of_lt_ciSup [Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i :=
  let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h
  ⟨i, h⟩

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