English
Let g: α → C(Y, Z) and f: α → C(X, Y). If g → g₀ and f → f₀ in the compact-open topology, then a ↦ g(a) ∘ f(a) → g₀ ∘ f₀ in C(X, Z).
Русский
Пусть g: α → C(Y,Z) и f: α → C(X,Y). Если g(a) → g₀ и f(a) → f₀ в компактно-открытой топологии, то a ↦ g(a) ∘ f(a) → g₀ ∘ f₀.
LaTeX
$$$\\operatorname{Tendsto}(a \\mapsto g(a)\\circ f(a))\\; l\\; (\\mathcal{N}(g_0\\circ f_0))$$$
Lean4
theorem _root_.Filter.Tendsto.compCM {α : Type*} {l : Filter α} {g : α → C(Y, Z)} {g₀ : C(Y, Z)} {f : α → C(X, Y)}
{f₀ : C(X, Y)} (hg : Tendsto g l (𝓝 g₀)) (hf : Tendsto f l (𝓝 f₀)) :
Tendsto (fun a ↦ (g a).comp (f a)) l (𝓝 (g₀.comp f₀)) :=
(continuous_comp'.tendsto (f₀, g₀)).comp (hf.prodMk_nhds hg)
