English
For every n and i, the map l ↦ Vector.eraseIdx i at l is continuous, i.e., ContinuousAt (Vector.eraseIdx i) l for all l ∈ Vector α (n+1).
Русский
Для каждого n и i отображение l ↦ Vector.eraseIdx i в позиции l непрерывно, то есть ContinuousAt (Vector.eraseIdx i) l для всех l ∈ Vector α (n+1).
LaTeX
$$$\\\\forall {\\\\n}, {i: Fin(n+1)}, \\\\forall {l: Vector(\\\\alpha, n+1)}, \\\\text{ContinuousAt}(\\\\text{Vector.eraseIdx } i) l$$$
Lean4
theorem continuousAt_eraseIdx {n : ℕ} {i : Fin (n + 1)} : ∀ {l : Vector α (n + 1)}, ContinuousAt (Vector.eraseIdx i) l
| ⟨l, hl⟩ => by
rw [ContinuousAt, Vector.eraseIdx, tendsto_subtype_rng]
simp only [Vector.eraseIdx_val]
exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val
