comp_tendsto — Mathlib

English

If f = O[l] g, then composing with k that tends to l' from l yields f ∘ k = O[l'] g ∘ k.

Русский

Если f = O_l(g), композиция с k, сходящимся к l, даёт f∘k = O_l' (g∘k).

LaTeX

$$$ \text{IsBigO}(l,f,g) \Rightarrow \text{IsBigO}(l', f\circ k, g\circ k) \text{ if } \text{Tendsto } k\ l'\ l $$$

Lean4

theorem comp_tendsto (hfg : f =O[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) : (f ∘ k) =O[l'] (g ∘ k) :=
  isBigO_iff_isBigOWith.2 <| hfg.isBigOWith.imp fun _c h => h.comp_tendsto hk

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