linearGrowthSup_nonneg

Mathlib.Analysis.Asymptotics.LinearGrowth

URI: https://scilib.ai/kg/mathlib#Monotone.linearGrowthSup_nonneg

← MathLib Explorer

English

If u is monotone and not bottom, then linearGrowthSup(u) ≥ 0.

Русский

Если функция u монотонна и не равна нижнему элементу, то linearGrowthSup(u) не меньше нуля.

LaTeX

$$$0 \le \operatorname{linearGrowthSup}(u)$$$

Lean4

theorem _root_.Monotone.linearGrowthSup_nonneg (h : Monotone u) (h' : u ≠ ⊥) : 0 ≤ linearGrowthSup u :=
  (h.linearGrowthInf_nonneg h').trans (linearGrowthInf_le_linearGrowthSup)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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