linearGrowthInf_monotone

Mathlib.Analysis.Asymptotics.LinearGrowth

URI: https://scilib.ai/kg/mathlib#LinearGrowth.linearGrowthInf_monotone

← MathLib Explorer

English

If u ≤ v as functions on ℕ, then linearGrowthInf(u) ≤ linearGrowthInf(v).

Русский

Если u(n) ≤ v(n) для всех n, то linearGrowthInf(u) ≤ linearGrowthInf(v).

LaTeX

$$$ \\text{linearGrowthInf}(u) \\le \\text{linearGrowthInf}(v) $$$

Lean4

theorem linearGrowthInf_monotone (h : u ≤ v) : linearGrowthInf u ≤ linearGrowthInf v :=
  linearGrowthInf_eventually_monotone (Eventually.of_forall h)

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

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

Разделы

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

Аффилиация

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