comp_tendsto — Mathlib

English

If f =o[𝕜; l] g and k tends to l, then f ∘ k = o[𝕜; lb] g ∘ k for lb = Tendsto k lb l.

Русский

Если f = o[𝕜; l] g и k стремится к l, тогда f ∘ k = o[𝕜; lb] g ∘ k для lb = Tendsto k lb l.

LaTeX

$$$h : 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) :=
  isLittleOTVS_map.mp (h.mono hk)

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