English
For every n ∈ ℕ and every list l, the map L ↦ eraseIdx L n is continuous at L = l; i.e., the function L ↦ L.eraseIdx n is continuous with respect to nhds l.
Русский
Для каждого n ∈ ℕ и каждой строки l функция L ↦ L.eraseIdx n непрерывна в точке L = l; то есть L ↦ L.eraseIdx n непрерывна по топологии nhds l.
LaTeX
$$$\\\\forall n \\\\forall l \\\\in \\\\text{List}(\\\\alpha), \\\\text{Tendsto}(\\\\lambda L: \\\\text{List}(\\\\alpha), L.\\\\text{eraseIdx} n)(\\\\mathcal{N}(l))(\\\\mathcal{N}(l.\\\\eraseIdx n))$$$
Lean4
theorem tendsto_eraseIdx : ∀ {n : ℕ} {l : List α}, Tendsto (eraseIdx · n) (𝓝 l) (𝓝 (eraseIdx l n))
| _, [] => by rw [nhds_nil]; exact tendsto_pure_nhds _ _
| 0, a :: l => by rw [tendsto_cons_iff]; exact tendsto_snd
| n + 1, a :: l => by
rw [tendsto_cons_iff]
dsimp [eraseIdx]
exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)
