isLittleO_const_smul_left — Mathlib

English

If f'' = o_l g'' and g'' → 0 along l, then f'' → 0 along l.

Русский

Если f'' = o_l g'' и g'' → 0 вдоль l, тогда f'' → 0 вдоль l.

LaTeX

$$$ (f'' =o[l] g'') \land (Tendsto g'' l (\mathcal{N}0)) \Rightarrow Tendsto f'' l (\mathcal{N}0). $$$

Lean4

theorem isLittleO_const_smul_left {c : 𝕜} (hc : c ≠ 0) : (fun x => c • f' x) =o[l] g ↔ f' =o[l] g :=
  by
  have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_left]
  simp only [norm_smul]
  rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

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