mul — Mathlib

English

If f1 = O l g1 and f2 = o l g2, then f1·f2 = o l g1·g2.

Русский

Если f1 = O_l(g1) и f2 = o_l(g2), то f1·f2 = o_l(g1·g2).

LaTeX

$$$\text{IsBigO}(l, f_1, g_1) \land \text{IsLittleO}(l, f_2, g_2) \Rightarrow \text{IsLittleO}(l, (f_1 f_2), (g_1 g_2)).$$$

Lean4

theorem mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
    (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x :=
  let ⟨_c, hc⟩ := h₁.isBigOWith
  let ⟨_c', hc'⟩ := h₂.isBigOWith
  (hc.mul hc').isBigO

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