English
For any fixed n, i ∈ Fin(n+1), and continuous maps f: β → α and g: β → Vector α n, the map b ↦ Vector.insertIdx (f b) i (g b) is continuous.
Русский
Для любых n, i ∈ Fin(n+1) и непрерывных отображений f: β → α, g: β → Vector α n, отображение b ↦ Vector.insertIdx (f b) i (g b) непрерывно.
LaTeX
$$$\\\\forall {\\\\beta}, {f:\\\\beta \\to \\\\alpha}, {g:\\\\beta \\to \\\\text{Vector}(\\\\alpha,n)}, \\\\text{Continuous} f \\rightarrow \\\\text{Continuous} g \\rightarrow \\\\text{Continuous}(\\\\lambda b: \\\\beta, \\\\text{Vector.insertIdx}(f b) i (g b))$$$
Lean4
theorem continuous_insertIdx {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → Vector α n} (hf : Continuous f)
(hg : Continuous g) : Continuous fun b => Vector.insertIdx (f b) i (g b) :=
continuous_insertIdx'.comp (hf.prodMk hg)
