natCast_atTop — Mathlib

English

If a function on a ring R has Big-O with respect to a bound, then after casting to naturals the same Big-O relation holds.

Русский

Если функция на кольце R имеет отношение Big-O, то после приведения к натуральным тем же свойством сохраняется.

LaTeX

$$$\\displaystyle \\text{If } f = O[atTop] g, \\; \\text{then } f\\circ cast = O[atTop] (g\\circ cast).$$$

Lean4

theorem natCast_atTop {R : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : R → E}
    {g : R → F} (h : f =O[atTop] g) : (fun (n : ℕ) => f n) =O[atTop] (fun n => g n) :=
  IsBigO.comp_tendsto h tendsto_natCast_atTop_atTop

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