const_smul_self — Mathlib

English

If f = O_l g and E is a module with a bounded scalar action, then c' · f is O_l g for any scalar c'.

Русский

Если f = O_l g и действует ограниченная скалярная билильная операция, то c' · f = O_l g для любого скаляра c'.

LaTeX

$$$ \text{If } f =O[l] g \text{ and } (c' f) \text{ is bounded}, \ c' \in R \Rightarrow (c' f) =O[l] g. $$$

Lean4

theorem const_smul_self (c' : R) : IsBigOWith (‖c'‖) l (fun x => c' • f' x) f' :=
  isBigOWith_of_le' _ fun _ => norm_smul_le _ _

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