English
Let f: α → ∀ j : Fin n, X (Fin.castSucc j) and g: α → X (Fin.last n) be functions, and s ⊆ α. If f and g are continuous within at a, then the function a ↦ Fin.snoc (f(a)) (g(a)) is continuous within at a.
Русский
Пусть f: α → ∀ j : Fin n, X (Fin.castSucc j) и g: α → X (Fin.last n). Пусть s ⊆ α. Если f и g непрерывны в точке a относительно s, то a ↦ Fin.snoc(f(a), g(a)) непрерывно в a относительно s.
LaTeX
$$$\\forall i\\;{f: \\alpha \\to \\forall j:\\mathrm{Fin}(n),X(j.castSucc)},\\{g: \\alpha \\to X(\\mathrm{Fin.last}\, n)\\},\\forall a\\in s,\\\\ContinuousWithinAt f\\ s\\ a \\land ContinuousWithinAt g\\ s\\ a \\Rightarrow \\text{ContinuousWithinAt } (a \\mapsto \\mathrm{Fin.snoc}(f(a), g(a)))\\ s\\ a$$$
Lean4
theorem finSnoc {f : α → ∀ j : Fin n, X (Fin.castSucc j)} {g : α → X (Fin.last _)} {a : α} {s : Set α}
(hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
ContinuousWithinAt (fun a => Fin.snoc (f a) (g a)) s a :=
hf.tendsto.finSnoc hg
