linearGrowthInf_le_linearGrowthSup_of_frequently_le

English

If u(n) ≤ v(n) holds for infinitely many n (frequently), then linearGrowthInf(u) ≤ linearGrowthSup(v).

Русский

Если неравенство u(n) ≤ v(n) выполняется для бесконечного числа элементов (часто встречается), то linearGrowthInf(u) ≤ linearGrowthSup(v).

LaTeX

$$$\bigl(\exists^{\infty} n \in \mathbb{N},\; u(n) \le v(n)\bigr) \implies \operatorname{linearGrowthInf}(u) \le \operatorname{linearGrowthSup}(v).$$$

Lean4

theorem linearGrowthInf_le_linearGrowthSup_of_frequently_le (h : ∃ᶠ n in atTop, u n ≤ v n) :
    linearGrowthInf u ≤ linearGrowthSup v :=
  (liminf_le_limsup_of_frequently_le) <| h.mono fun n u_v ↦ by gcongr

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