trans_tendsto — Mathlib

English

For any l and c, f = O_l (λ x, c) is equivalent to (c = 0 → f is eventually zero) and IsBoundedUnder (≤) l (‖f‖).

Русский

Для любых l и c, f = O_l (λ x, c) эквивалентно (c = 0 → f ≡ 0 на l) и IsBoundedUnder (≤) l (‖f‖).

LaTeX

$$$ (f =O[l](\lambda x. c)) \iff \big( c = 0 \to l\text{-eventually } f = 0 \big) \land IsBoundedUnder (\le) l (\|f\|). $$$

Lean4

theorem trans_tendsto (hfg : f'' =O[l] g'') (hg : Tendsto g'' l (𝓝 0)) : Tendsto f'' l (𝓝 0) :=
  (isLittleO_one_iff ℝ).1 <| hfg.trans_isLittleO <| (isLittleO_one_iff ℝ).2 hg

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