const_mul_right' — Mathlib

English

If IsUnit c and IsBigO l f (c·g) then IsBigO l f g.

Русский

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

LaTeX

$$$\text{IsBigO}(l, f, (c\cdot g)) \Rightarrow \text{IsBigO}(l, f, g), \text{ если } c \text{ — единица.}$$$

Lean4

theorem const_mul_right' {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0 ≤ c') (h : IsBigOWith c' l f g) :
    IsBigOWith (c' * ‖(↑u⁻¹ : R)‖) l f fun x => ↑u * g x :=
  h.trans (isBigOWith_self_const_mul' _ _ _) hc'

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