ciInf_of_not_bddBelow

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If the range of f is not bounded below, then the infimum over i of f i equals sInf ∅.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ciInf_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf ∅ :=
  csInf_of_not_bddBelow hf

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

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

Разделы

Аффилиация

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