English
If two families of elements converge coordinatewise in corresponding finite-dimensional product spaces, then the coordinatewise snoc (append) construction also converges to the single snoc of the limits. More precisely, if f: Y → ∀ j ∈ Fin n, A j.castSucc tends to x and g: Y → A (Fin.last _) tends to y, then the map a ↦ Fin.snoc(f(a), g(a)) tends to Fin.snoc(x, y).
Русский
Если каждое из двух семей элементов сходится по координатам в соответствующих конечномерных произведениях, то операция добавления последнего элемента (snoc) выполняется непрерывно по отношению к пределам. Точнее: если f: Y → ∀ j ∈ Fin n, A j.castSucc сходится к x и g: Y → A (Fin.last _) сходится к y, то a ↦ Fin.snoc(f(a), g(a)) сходится к Fin.snoc(x, y).
LaTeX
$$$\\displaystyle \\text{Tendsto}\\bigl( a \\mapsto \\mathrm{Fin.snoc}\\bigl( f(a) , g(a) \\bigr) \\bigr) \\, l \\, \\mathcal{N}\\bigl( \\mathrm{Fin.snoc}(x,y) \\bigr).$$$
Lean4
theorem finSnoc {f : Y → ∀ j : Fin n, A j.castSucc} {g : Y → A (Fin.last _)} {l : Filter Y}
{x : ∀ j, A (Fin.castSucc j)} {y : A (Fin.last _)} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
Tendsto (fun a => Fin.snoc (f a) (g a)) l (𝓝 <| Fin.snoc x y) :=
tendsto_pi_nhds.2 fun j => Fin.lastCases (by simpa) (by simpa using tendsto_pi_nhds.1 hf) j
