isBigO_const_mul_left_iff' — Mathlib

English

If c is a unit, then left-multiplying f by c does not affect its Big-O relation with g; i.e., (c f) = O_l g iff f = O_l g.

Русский

Если c — единица (обратимый элемент), то левое умножение на c не меняет отношение Big-O: (c f) = O_l(g) эквивалентно f = O_l(g).

LaTeX

$$$\text{IsBigO}_l\left(f, g\right) \iff \text{IsBigO}_l\left(c\,f, g\right), \text{ если } c \text{ — единица по норме}.$$$

Lean4

theorem isBigO_const_mul_left_iff' {f : α → R} {c : R} (hc : IsUnit c) : (fun x => c * f x) =O[l] g ↔ f =O[l] g :=
  ⟨(isBigO_self_const_mul' hc f l).trans, fun h => h.const_mul_left c⟩

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