English
If f: Y → A_i and g: Y → ∀ j : Fin n, A (i.succAbove j) converge to x and y respectively, then the map a ↦ i.insertNth (f(a)) (g(a)) converges to i.insertNth(x)(y).
Русский
Если f и g сходятся к x и y соответственно, то a ↦ i.insertNth(f(a), g(a)) сходится к i.insertNth(x, y).
LaTeX
$$$\\displaystyle \\text{Tendsto}\\bigl( a \\mapsto i.insertNth\\bigl(f(a), g(a)\\bigr) \\bigr)\\; l\\; \\mathcal{N}\\bigl(i.insertNth(x,y)\\bigr).$$$
Lean4
theorem finInsertNth (i : Fin (n + 1)) {f : Y → A i} {g : Y → ∀ j : Fin n, A (i.succAbove j)} {l : Filter Y} {x : A i}
{y : ∀ j, A (i.succAbove j)} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
Tendsto (fun a => i.insertNth (f a) (g a)) l (𝓝 <| i.insertNth x y) :=
tendsto_pi_nhds.2 fun j => Fin.succAboveCases i (by simpa) (by simpa using tendsto_pi_nhds.1 hg) j
