of_const_mul_right — Mathlib

English

If c is a unit, then IsBigOWith c' l f g implies IsBigOWith c' l f (c·g).

Русский

Если c — единица, то IsBigOWith c' l f g → IsBigOWith c' l f (c·g).

LaTeX

$$$\text{IsBigOWith}(c', l, f, g) \Rightarrow \text{IsBigOWith}(c', l, f, (c\cdot g)).$$$

Lean4

theorem of_const_mul_right {g : α → R} {c : R} (hc' : 0 ≤ c') (h : IsBigOWith c' l f fun x => c * g x) :
    IsBigOWith (c' * ‖c‖) l f g :=
  h.trans (isBigOWith_const_mul_self c g l) hc'

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