ciInf_lt_iff

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#ciInf_lt_iff

← MathLib Explorer

English

For Nonempty ι, iInf f < a iff ∃ i, f(i) < a (dual form of Inf).

Русский

Для непустого ι: iInf f < a эквивалентно ∃ i, f(i) < a.

LaTeX

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

Lean4

theorem ciInf_lt_iff [Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) : iInf f < a ↔ ∃ i, f i < a := by
  simpa only [mem_range, exists_exists_eq_and] using csInf_lt_iff hb (range_nonempty _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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