isBigO_self_const_mul' — Mathlib

English

If c is a unit in a normed ring, then f = O_l(g) implies c · f = O_l(g) and vice versa up to unit equivalence.

Русский

Если c единица в нормированной кольце, то f = O_l(g) эквивалентно c f = O_l(g) (и наоборот) с учётом единиц.

LaTeX

$$isBigO_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) : IsBigO l (fun x => c * f x) g$$

Lean4

theorem isBigO_self_const_mul' {c : R} (hc : IsUnit c) (f : α → R) (l : Filter α) : f =O[l] fun x => c * f x :=
  let ⟨u, hu⟩ := hc
  hu ▸ (isBigOWith_self_const_mul' u f l).isBigO

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