smul — Mathlib

English

If k1 = o_l(k2) and f' = o_l(g'), then the product-valued function x ↦ k1(x) • f'(x) is little-o of x ↦ k2(x) • g'(x) with respect to l.

Русский

Пусть k1 = o_l(k2) и f' = o_l(g'). Тогда функция x ↦ k1(x) · f'(x) является малым-o по отношению к функции x ↦ k2(x) · g'(x) при x→ лямде l.

LaTeX

$$$ (k_1 =o[l] k_2) \land (f' =o[l] g') \\Rightarrow (fun x => k_1 x \\cdot f' x) =o[l] (fun x => k_2 x \\cdot g' x) $$$

Lean4

theorem smul (h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') : (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x :=
  h₁.smul_isBigO h₂.isBigO

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