exists_lt_of_ciInf_lt — Mathlib

English

If iInf f < a for a, there exists i with f(i) < a (indexed version).

Русский

Если iInf f меньше a, то существует i, для которого f(i) < a.

LaTeX

$$$\text{If } iInf f < a, \text{ then } \exists i, f(i) < a.$$$

Lean4

/-- Indexed version of `exists_lt_of_csInf_lt`.
When `iInf f < a`, there is an element `i` such that `f i < a`.
-/
theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a :=
  exists_lt_of_lt_ciSup (α := αᵒᵈ) h

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