linearGrowthInf_natCast_nonneg — Mathlib

English

Let v: N → N. Interpreting v(n) as an extended-real, every value is nonnegative, hence the lower linear growth infimum of the sequence is nonnegative:

Русский

Пусть v: ℕ → ℕ. Рассматривая v(n) как элемент расширенного множества вещественных, все значения неотрицательны, следовательно нижний инфимум линейного роста последовательности неотрицателен:

LaTeX

$$$0 \le \operatorname{linearGrowthInf}\bigl( n \mapsto (v(n) : \mathbb{E}) \bigr)$$$

Lean4

theorem linearGrowthInf_natCast_nonneg (v : ℕ → ℕ) : 0 ≤ linearGrowthInf fun n ↦ (v n : EReal) :=
  (le_liminf_of_le) (Eventually.of_forall fun n ↦ div_nonneg (v n).cast_nonneg' n.cast_nonneg')

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