English
Let f: ℝ → E and g: ℝ → F be functions and suppose f(x) = o_{atTop}(g(x)) as x → +∞. Then the sequence a_n = f(n) is o_{atTop} of the sequence b_n = g(n), i.e., a_n = o(b_n) as n → ∞ when n is regarded as a real via the natural embedding.
Русский
Пусть f: ℝ → E и g: ℝ → F, и предположим, что f(x) = o_{atTop}(g(x)) при x → +∞. Тогда последовательность a_n = f(n) является малым по отношению к b_n = g(n) при n → ∞, когда аргументы n рассматриваются как элементы ℝ через естественное вложение.
LaTeX
$$$ (f \\circ \\iota) = o_{atTop} (g \\circ \\iota) $$$
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) :=
IsLittleO.comp_tendsto h tendsto_natCast_atTop_atTop
