English
Let i ∈ Fin(n+1). If f: α → X i is continuous on s and g: α → ∀ j : Fin n, X (i.succAbove j) is continuous on s, then the function a ↦ i.insertNth (f a) (g a) is continuous on s.
Русский
Пусть i ∈ Fin(n+1). Если f: α → X i и g: α → ∀ j : Fin n, X(i.succAbove j) непрерывны на s, тогда a ↦ i.insertNth(f(a))(g(a)) непрерывна на s.
LaTeX
$$$\\forall i:\\mathrm{Fin}(n+1),\\; (\\text{ContinuousWithinAt } f\\ s\\ a) \\land (\\text{ContinuousWithinAt } g\\ s\\ a) \\Rightarrow \\text{ContinuousWithinAt } (a \\mapsto i.insertNth (f(a)) (g(a)))\\ s\\ a$$$
Lean4
theorem finInsertNth (i : Fin (n + 1)) {f : α → X i} {g : α → ∀ j : Fin n, X (i.succAbove j)} {a : α} {s : Set α}
(hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) :
ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a :=
hf.tendsto.finInsertNth i hg
