English
If f is continuous on s and g is continuous on s, then a ↦ Fin.snoc (f a) (g a) is continuous on s.
Русский
Если f и g непрерывны на s, то a ↦ Fin.snoc (f(a)) (g(a)) непрерывна на s.
LaTeX
$$$\\forall f: \\alpha \\to \\forall j:\\mathrm{Fin}(n),X(j.castSucc),\\forall g: \\alpha \\to X(\\mathrm{Fin.last}\\, n),\\forall s:\\Set\\alpha,\\; (\\text{ContinuousOn } f\\ s) \\land (\\text{ContinuousOn } g\\ s) \\Rightarrow \\text{ContinuousOn } (a \\mapsto \\mathrm{Fin.snoc}(f(a), g(a)))\\ s$$$
Lean4
theorem finSnoc {f : α → ∀ j : Fin n, X (Fin.castSucc j)} {g : α → X (Fin.last _)} {s : Set α} (hf : ContinuousOn f s)
(hg : ContinuousOn g s) : ContinuousOn (fun a => Fin.snoc (f a) (g a)) s := fun a ha => (hf a ha).finSnoc (hg a ha)
