le_ciInf_iff'

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

For Nonempty ι, a ≤ iInf f iff ∀ i, a ≤ f i.

Русский

Для непустого множества индексов ι верно: a ≤ iInf f ⇔ ∀ i, a ≤ f(i).

LaTeX

$$$ a \le \inf_{i} f(i) \iff \forall i, a \le f(i) $$$

Lean4

theorem le_ciInf_iff' [Nonempty ι] {f : ι → α} {a : α} : a ≤ iInf f ↔ ∀ i, a ≤ f i :=
  le_ciInf_iff (OrderBot.bddBelow _)

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

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

Разделы

Аффилиация

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