comp_tendsto — Mathlib

English

IsLittleO l f g is equivalent to IsBigOWith c l f g for some c > 0, and map preserves this equivalence.

Русский

IsLittleO l f g эквивалентно IsBigOWith c l f g для некоторого c>0, и отображение сохраняет эквивалентность через map.

LaTeX

$$$ IsLittleO\ l\ f\ g \iff IsBigOWith\ c\ l\ f\ g \text{ для некоторого } c>0 $$$

Lean4

theorem comp_tendsto (hfg : f =o[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) : (f ∘ k) =o[l'] (g ∘ k) :=
  IsLittleO.of_isBigOWith fun _c cpos => (hfg.forall_isBigOWith cpos).comp_tendsto hk

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