biInf_le_eq_iInf

Mathlib.Order.CompleteLattice.Basic

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

English

In a preordered lattice, infimum with index j ≤ i equals infimum over i of f i.

Русский

В предпорядке инфимум с индексом j ≤ i равен инфимуму по i.

LaTeX

$$$ \\inf_{i} \\inf_{j \\le i} f(j) = \\inf_{i} f(i). $$$

Lean4

theorem biInf_le_eq_iInf {ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≤ i), f j = ⨅ i, f i :=
  biSup_le_eq_iSup (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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