comp_tendsto — Mathlib

English

The big-OTVS relation is preserved under precomposition with a Tendsto map: if f =O[𝕜; l] g and k tends to l, then f ∘ k =O[𝕜; lb] g ∘ k.

Русский

Отношение Big-OTVS сохраняется под предкомпозицию через предел Tendsto: если f =O[𝕜; l] g и k стремится к l, то f ∘ k =O[𝕜; lb] g ∘ k.

LaTeX

$$$f =O[𝕜; l] g \\land hk : Tendsto k\\ lb\\ l \\Rightarrow (f \\circ k) =O[𝕜; lb] (g \\circ k).$$$

Lean4

theorem comp_tendsto {k : β → α} {lb : Filter β} (h : f =O[𝕜; l] g) (hk : Tendsto k lb l) : (f ∘ k) =O[𝕜; lb] (g ∘ k) :=
  isBigOTVS_map.mp (h.mono hk)

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