isLittleO_const_mul_right_iff' — Mathlib

English

If hc : 0 ≤ c' and h : IsBigOWith c' l f (c·g) then IsBigOWith (c'·‖c‖) l f g.

Русский

Если 0 ≤ c' и f =OWith c' l f (c g), то f =OWith (c' |c|) l f g.

LaTeX

$$$0 \le c' \Rightarrow IsBigOWith(c', l, f, (c\cdot g)) \Rightarrow IsBigOWith(c'\cdot \|c\|, l, f, g).$$$

Lean4

theorem isLittleO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) : (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
  ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

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