isGLB_ciInf

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

Let a be a lower bound for all products g(i)·h(j). Then a ≤ (inf_i g(i))·(inf_j h(j)).

Русский

Пусть a ≤ g(i)·h(j) для всех i,j. Тогда a ≤ (inf_i g(i))·(inf_j h(j)).

LaTeX

$$$\displaystyle \forall i,\forall j,\ a \le g(i)\cdot h(j) \Rightarrow a \le (\inf_i g(i))\cdot (\inf_j h(j))$$$

Lean4

theorem isGLB_ciInf [Nonempty ι] {f : ι → α} (H : BddBelow (range f)) : IsGLB (range f) (⨅ i, f i) :=
  isGLB_csInf (range_nonempty f) H

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

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

Разделы

Аффилиация

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