isLittleO_const_mul_right_iff — Mathlib

English

If IsBigO l f (c·g) holds with unit c, then IsBigO l f g holds.

Русский

Если IsBigO l f (c g) держится при единице c, тогда IsBigO l f g держится.

LaTeX

$$$\text{IsBigO}(l, f, (c\cdot g)) \Rightarrow \text{IsBigO}(l, f, g), \text{ при } c \in \text{Units}. $$$

Lean4

theorem isLittleO_const_mul_right_iff {g : α → S} {c : S} (hc : c ≠ 0) : (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
  ⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.trans_isBigO (isBigO_self_const_mul hc g l)⟩

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