biInf_lt_eq_iInf

Mathlib.Order.CompleteLattice.Basic

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

English

Under dual order, the infimum over i with j < i collapses to a single iInf expression.

Русский

Под двойственным порядком инфимуум над i с j < i сводится к одному выражению iInf.

LaTeX

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

Lean4

theorem biInf_lt_eq_iInf {ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} : ⨅ (i) (j < i), f j = ⨅ i, f i :=
  biSup_lt_eq_iSup (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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