continuous_insertIdx — Mathlib

English

Let α be a topological space. For every n ∈ ℕ, the map (a, l) ↦ l.insertIdx n a from α × List α to List α is continuous.

Русский

Пусть α — топологическое пространство. Для любого n ∈ ℕ отображение (a, l) ↦ l.insertIdx n a из α × List α в List α непрерывно.

LaTeX

$$$\\\\forall a \\\\forall l \\\\forall n \\\\in \\\\mathbb{N}, \\\\\\\\text{Continuous}( \\\\lambda p:(\\\\alpha \\\\times \\\\text{List}(\\\\alpha)), p.2.insertIdx n p.1 )$$$

Lean4

theorem continuous_insertIdx {n : ℕ} : Continuous fun p : α × List α => p.2.insertIdx n p.1 :=
  continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx'

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