exists_lt_of_lt_ciSup'

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#exists_lt_of_lt_ciSup'

English

If a < iSup f, then there exists i with a < f i.

Русский

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

LaTeX

$$$ a < \sup_{i} f(i) \Rightarrow \exists i, a < f(i) $$$

Lean4

theorem exists_lt_of_lt_ciSup' {f : ι → α} {a : α} (h : a < ⨆ i, f i) : ∃ i, a < f i :=
  by
  contrapose! h
  exact ciSup_le' h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru