English
Let F be a function-like object with a domain α and codomain X, and let f: ι → F tend to g in the sense of the neighborhood of g. Then for every a ∈ α the evaluations f(i)(a) converge to g(a) as i tends to the same limit.
Русский
Пусть F — множество функций с областью α и кодом X, пусть f: ι → F стремится к g в окрестности g; тогда для каждого a ∈ α последовательность значений f(i)(a) сходится к g(a).
LaTeX
$$$\forall {\iota} {l} {f : \iota \to F} {g : F},\ (\\ Tendsto\ f\ l\ (nhds\ g)) \ \Rightarrow\ \forall a : \alpha,\ Tendsto (\\lambda i, (f i) a) l (nhds (g a))$$$
Lean4
protected theorem eval_const {ι : Type*} {l : Filter ι} {f : ι → F} {g : F} (hf : Tendsto f l (𝓝 g)) (a : α) :
Tendsto (f · a) l (𝓝 (g a)) :=
((continuous_id.eval_const a).tendsto _).comp hf
