English
For a fixed index i in Fin(n+1), the operation of removing the i-th entry from a vector is continuous as a function on vectors.
Русский
Для фиксированного индекса i ∈ Fin(n+1) операция удаления i-й компоненты вектора непрерывна по отношению к векторному пространству.
LaTeX
$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], \\\\forall {n}, \\\\forall {i: Fin(n+1)}, \\\\text{Continuous}( \\\\lambda v: \\\\text{Vector }\\\\alpha (n+1) \\\\,\\\\to \\\\text{Vector }\\\\alpha n, \\\\text{Vector.eraseIdx } i \, v )$$$
Lean4
theorem continuous_eraseIdx {n : ℕ} : Continuous fun l : List α => eraseIdx l n :=
continuous_iff_continuousAt.mpr fun _a => tendsto_eraseIdx
