smul — Mathlib

English

If IsBigOWith c l k1 k2 and IsBigOWith c' l f' g', then IsBigOWith (c*c') l (k1 • f') (k2 • g').

Русский

Если IsBigOWith c l k1 k2 и IsBigOWith c' l f' g', тогда IsBigOWith (c*c') l (k1 • f') (k2 • g').

LaTeX

$$$ IsBigOWith c l k1 k2 \land IsBigOWith c' l f' g' \Rightarrow IsBigOWith (c*c') l (\lambda x. k1 x • f' x) (\lambda x. k2 x • 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 :=
  by
  obtain ⟨c₁, h₁⟩ := h₁.isBigOWith
  obtain ⟨c₂, h₂⟩ := h₂.isBigOWith
  exact (h₁.smul h₂).isBigO

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