English
Continuity of insertIdx with respect to Tendsto on the tail of a list.
Русский
Непрерывность insertIdx по отношению к Tendsto для хвоста списка.
LaTeX
$$$ \forall a, n, l,\; \operatorname{Tendsto}(\lambda p: p.2.insertIdx n p.1)(\mathcal{N}(a) \times\mathcal{N}(l))(\mathcal{N}(l.\operatorname{insertIdx} n a)) $$$
Lean4
/-- Continuity of `insertIdx` in terms of `Tendsto`. -/
theorem tendsto_insertIdx' {a : α} :
∀ {n : ℕ} {l : List α}, Tendsto (fun p : α × List α => p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 (l.insertIdx n a))
| 0, _ => tendsto_cons
| n + 1, [] => by simp
| n + 1, a' :: l =>
by
have : 𝓝 a ×ˢ 𝓝 (a' :: l) = (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1 :: p.2.2) :=
by
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
simp [-Filter.map_def, Function.comp_def, functor_norm]
rw [this, tendsto_map'_iff]
exact
(tendsto_fst.comp tendsto_snd).cons
((@tendsto_insertIdx' _ n l).comp <| tendsto_fst.prodMk <| tendsto_snd.comp tendsto_snd)
