comp_tendsto — Mathlib

English

IsBigOWith c l f g is equivalent to IsBigOWith c (Filter.map k l) (f ∘ k) (g ∘ k).

Русский

IsBigOWith c l f g эквивалентно IsBigOWith c (map k l) (f ∘ k) (g ∘ k).

LaTeX

$$$ IsBigOWith\ c\ (map\ k\ l)\ f\ g \;\equiv\; IsBigOWith\ c\ l\ (f \circ k) (g \circ k) $$$

Lean4

theorem comp_tendsto (hcfg : IsBigOWith c l f g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) :
    IsBigOWith c l' (f ∘ k) (g ∘ k) :=
  IsBigOWith.of_bound <| hk hcfg.bound

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