comp_tendsto — Mathlib

English

If f is asymptotically equivalent to g along l', and k tends to l', then f∘k is asymptotically equivalent to g∘k along l.

Русский

Если f эквивалентно g по l' и k tends to l', то f∘k эквивалентно g∘k по l.

LaTeX

$$f ~[l'] g \Rightarrow \forall k, (Filter.Tendsto k l l') \Rightarrow (f \circ k) ~[l] (g \circ k)$$

Lean4

theorem comp_tendsto {α₂ : Type*} {f g : α₂ → β} {l' : Filter α₂} (hfg : f ~[l'] g) {k : α → α₂}
    (hk : Filter.Tendsto k l l') : (f ∘ k) ~[l] (g ∘ k) :=
  IsLittleO.comp_tendsto hfg hk

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