English
If f converges to f0 and g converges to x0 along a filter l, then the composite a ↦ f(a)(g(a)) converges to f0(x0).
Русский
Если f стремится к f0, а g к x0 вдоль фильтра l, то композиция a ↦ f(a)(g(a)) стремится к f0(x0).
LaTeX
$$$\\text{Tendsto } f l (\\mathcal{N} f_0) \\; \\&\\; \\text{Tendsto } g l (\\mathcal{N} x_0) \\Rightarrow \\text{Tendsto } (a \\mapsto f(a)(g(a))) l (\\mathcal{N}(f_0 x_0))$$$
Lean4
protected theorem eval {α : Type*} {l : Filter α} {f : α → F} {f₀ : F} {g : α → X} {x₀ : X} (hf : Tendsto f l (𝓝 f₀))
(hg : Tendsto g l (𝓝 x₀)) : Tendsto (fun a ↦ f a (g a)) l (𝓝 (f₀ x₀)) :=
(ContinuousEval.continuous_eval.tendsto _).comp (hf.prodMk_nhds hg)
