English
The operation of cons-ing an element to a vector is continuous in the product topology: Tendsto (fun p => p.fst ::ᵥ p.snd) (nhds a × nhds l) (nhds (a ::ᵥ l)).
Русский
Операция добавления элемента слева к вектору непрерывна в произведённой топологии: Tendsto (p.fst ::ᵥ p.snd) (nhds a × nhds l) nhds (a ::ᵥ l).
LaTeX
$$$\\\\text{Tendsto}(\\\\lambda p: (\\\\alpha \\\\times \\\\text{Vector}(\\\\alpha,n)), p.1 ::ᵥ p.2) (\\\\mathcal{N} a \\\\timesˢ \\\\mathcal{N} l) \\\\rightarrow \\\\mathcal{N}(a ::ᵥ l)$$$
Lean4
theorem tendsto_cons {n : ℕ} {a : α} {l : Vector α n} :
Tendsto (fun p : α × Vector α n => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l)) :=
by
rw [tendsto_subtype_rng, Vector.cons_val]
exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)
