tendsto_atTop_r_real — Mathlib

English

For each i, r_i(n) tends to infinity along natural numbers, i.e., Tendsto (r_i) atTop atTop.

Русский

Для каждого i функция r_i(n) достигает бесконечности по естественным числам, то есть Tendsto (r_i) atTop atTop.

LaTeX

$$$\forall i,\; \text{Tendsto}(r_i)\;\text{atTop}\;\text{atTop}$$$

Lean4

theorem tendsto_atTop_r_real (i : α) : Tendsto (fun n => (r i n : ℝ)) atTop atTop :=
  Tendsto.comp tendsto_natCast_atTop_atTop (R.tendsto_atTop_r i)

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