English
If f tends to b and g tends to l, then the pair (f, g) tends to (b :: l) through cons.
Русский
Если f стремится к b, а g — к l, то пара (f, g) стремится к (b :: l) через операцию cons.
LaTeX
$$$ \operatorname{Tendsto} \big( a \mapsto \operatorname{List}.cons (f(a)) (g(a)) \big)\ a\ ( \mathcal{N}(b) \ast \mathcal{N}(l) ) \Rightarrow \operatorname{Tendsto} \big( a \mapsto \operatorname{List}.cons (f(a)) (g(a)) \big) a (\mathcal{N}(b :: l)) $$$
Lean4
theorem cons {α : Type*} {f : α → β} {g : α → List β} {a : Filter α} {b : β} {l : List β} (hf : Tendsto f a (𝓝 b))
(hg : Tendsto g a (𝓝 l)) : Tendsto (fun a => List.cons (f a) (g a)) a (𝓝 (b :: l)) :=
List.tendsto_cons.comp (Tendsto.prodMk hf hg)
