English
If f tends to a and g tends to l, then the function b ↦ (g b).insertIdx n (f b) tends to (l.insertIdx n a).
Русский
Если f стремится к a и g стремится к l, то функция b ↦ (g b).insertIdx n (f b) стремится к (l.insertIdx n a).
LaTeX
$$$ \operatorname{Tendsto} f\ b (\mathcal{N} a) \land \operatorname{Tendsto} g\ b (\mathcal{N} l) \Rightarrow \operatorname{Tendsto} (\lambda b, (g b).insertIdx n (f b))\ b (\mathcal{N}(l.insertIdx n a)) $$$
Lean4
theorem tendsto_insertIdx {β} {n : ℕ} {a : α} {l : List α} {f : β → α} {g : β → List α} {b : Filter β}
(hf : Tendsto f b (𝓝 a)) (hg : Tendsto g b (𝓝 l)) :
Tendsto (fun b : β => (g b).insertIdx n (f b)) b (𝓝 (l.insertIdx n a)) :=
tendsto_insertIdx'.comp (hf.prodMk hg)
