biInf_le_eq_inf

Mathlib.Order.CompleteLattice.Basic

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

English

In a complete lattice, for any index i and function f, the infimum up to i decomposes as ∧_{j<i} f(j) ⊓ f(i).

Русский

В полной решётке для любого i и функции f: inf_{j≤i} f(j) = inf_{j<i} f(j) ⊓ f(i).

LaTeX

$$$$ \bigwedge_{j \le i} f(j) = \left( \bigwedge_{j < i} f(j) \right) \wedge f(i) $$$$

Lean4

theorem biInf_le_eq_inf : (⨅ j ≤ i, f j) = (⨅ j < i, f j) ⊓ f i :=
  biSup_le_eq_sup (α := αᵒᵈ) f i

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

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

Разделы

Аффилиация

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