lt_ciSup_iff — Mathlib

English

For Nonempty ι and BddAbove range f, a < iSup f iff there exists i with a < f(i).

Русский

Для непустого ι и верхних границ диапазона f, a < iSup f эквивалентно существованию i, такого что a < f(i).

LaTeX

$$$\text{If } BddAbove(\mathrm{range}(f)):\ a < iSup f \iff \exists i, a < f(i).$$$

Lean4

theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i := by
  simpa only [mem_range, exists_exists_eq_and] using lt_csSup_iff hb (range_nonempty _)

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