English
Continuity of Vector.insertIdx: for every α with a topology and every n, i ∈ Fin(n+1), the map p ↦ Vector.insertIdx p.fst i p.snd is continuous.
Русский
Непрерывность Vector.insertIdx': для каждого α с топологией и каждого n, i ∈ Fin(n+1), отображение p.fst, p.snd → Vector.insertIdx p.fst i p.snd непрерывно.
LaTeX
$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], {n}, {i: Fin(n+1)}, \\\\text{Continuous}(\\\\lambda p: \\\\alpha \\\\times \\\\text{Vector}(\\\\alpha,n), \\\\text{Vector.insertIdx } p.fst i p.snd)$$$
Lean4
/-- Continuity of `Vector.insertIdx`. -/
theorem continuous_insertIdx' {n : ℕ} {i : Fin (n + 1)} :
Continuous fun p : α × Vector α n => Vector.insertIdx p.1 i p.2 :=
continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx
