ciInf_eq_univ_of_not_bddBelow

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If the range f is not bounded below, then ⨅ i, f i = sInf univ.

Русский

Если диапазон f не ограничен снизу, то ⋂ по i f(i) равен sInf univ.

LaTeX

$$$ \neg BddBelow(\mathrm{range}(f)) \Rightarrow \big( \inf_i f(i) = sInf univ \big)$$$

Lean4

theorem ciInf_eq_univ_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf univ :=
  csInf_eq_univ_of_not_bddBelow hf

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

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

Разделы

Аффилиация

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