iSup_of_not_bddAbove

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.iSup_of_not_bddAbove

English

Let f: I → NNReal have unbounded range. Then ⨆ i, f(i) = 0.

Русский

Пусть f: I → ℝ≥0 имеет неограниченное множество значений. Тогда ⨆ i, f(i) = 0.

LaTeX

$$$ \neg BddAbove(\mathrm{range}(f)) \Rightarrow \big( \sup_i f(i) = 0 \big).$$$

Lean4

theorem iSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = 0 :=
  sSup_of_not_bddAbove hf

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

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

Разделы

Аффилиация

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