English
Let i ∈ Fin(n+1). If f: α → X i and g: α → ∀ j : Fin n, X (i.succAbove j) are continuous on s, then the map 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{ContinuousOn } f\\ s) \\to (\\text{ContinuousOn } g\\ s) \\Rightarrow \\text{ContinuousOn } (a \\mapsto i.insertNth (f(a)) (g(a)))\\ s$$$
Lean4
theorem finInsertNth (i : Fin (n + 1)) {f : α → X i} {g : α → ∀ j : Fin n, X (i.succAbove j)} {s : Set α}
(hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun a => i.insertNth (f a) (g a)) s := fun a ha =>
(hf a ha).finInsertNth i (hg a ha)
