English
For any α with a topology, any finite n+1, any a ∈ α, and any l ∈ Vector α n, the map p ↦ Vector.insertIdx p.fst i p.snd is continuous in the product nhds of a and l, i.e., Tendsto (fun p => List.Vector.insertIdx p.fst i p.snd) (nhds a × nhds l) (nhds (Vector.insertIdx a i l)).
Русский
Для любой топологии на α и любых i ∈ Fin(n+1), a ∈ α и l ∈ Vector α n, отображение p ↦ Vector.insertIdx p.fst i p.snd непрерывно в произведении nhds: Tendsto (fun p => List.Vector.insertIdx p.fst i p.snd) (nhds a × nhds l) (nhds (Vector.insertIdx a i l)).
LaTeX
$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], {n}, {i: Fin(n+1)}, {a: \\alpha}, {l: Vector(\\\\alpha,n)}, \\\\text{Tendsto}(\\\\lambda p: (\\\\alpha \\\\times \\\\text{Vector}(\\\\alpha,n), \\text{Vector.insertIdx}(p.fst,i,p.snd)) (\\\\mathcal{N} a \\\\times \\\\mathcal{N} l) \\\\rightarrow \\\\mathcal{N}(\\\\text{Vector.insertIdx } a i l))$$$
Lean4
theorem tendsto_insertIdx {n : ℕ} {i : Fin (n + 1)} {a : α} :
∀ {l : Vector α n}, Tendsto (fun p : α × Vector α n => insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx a i l))
| ⟨l, hl⟩ => by
rw [insertIdx, tendsto_subtype_rng]
simp only [insertIdx_val]
exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)
