isGLB_iInf

Mathlib.Order.CompleteLattice.Basic

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

English

The infimum iInf f is the greatest lower bound of the range of f.

Русский

Инфиму́мум iInf f является наибольшей нижней гранью множества range f.

LaTeX

$$$$\\text{IsGLB}(\\operatorname{range}(f), \\iInf_i f(i)).$$$$

Lean4

theorem isGLB_iInf : IsGLB (range f) (⨅ j, f j) :=
  isGLB_sInf _

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

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

Разделы

Аффилиация

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