continuous_eraseIdx — Mathlib

English

The function Vector.eraseIdx i is continuous: for any i, the map Vector α (n+1) → Vector α n is continuous.

Русский

Функция Vector.eraseIdx i непрерывна: для любого i отображение Vector α (n+1) → Vector α n непрерывно.

LaTeX

$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], {n}, {i: Fin(n+1)}, \\\\text{Continuous}(\\\\text{Vector.eraseIdx } i)$$$

Lean4

theorem continuous_eraseIdx {n : ℕ} {i : Fin (n + 1)} :
    Continuous (Vector.eraseIdx i : Vector α (n + 1) → Vector α n) :=
  continuous_iff_continuousAt.mpr fun ⟨_a, _l⟩ => continuousAt_eraseIdx

Похожие утверждения