iInf_lt_iff

Mathlib.Order.CompleteLattice.Defs

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

English

In a complete linear order with InfSet, iInf f < a iff there exists i with f(i) < a.

Русский

В упорядоченном множестве с InfSet: iInf f < a тогда, когда существует i, для которого f(i) < a.

LaTeX

$$$iInf f < a \;\iff\; \exists i, f(i) < a$$$

Lean4

theorem iInf_lt_iff {f : ι → α} : iInf f < a ↔ ∃ i, f i < a :=
  sInf_lt_iff.trans exists_range_iff

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

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

Разделы

Аффилиация

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