English
A Tendsto to a cons state is equivalent to Tendsto of the components under a product structure.
Русский
Стремление к константному списку через разложение эквивалентно стремлению к компонентам в произведении.
LaTeX
$$$ \operatorname{Tendsto} f (\mathcal{N}(a \! :: \ l)) b \iff \operatorname{Tendsto} (\lambda p: a \times l, f(p.1 :: p.2)) (\mathcal{N}(a) \times^\mathsf{nhds} \mathcal{N}(l)) b $$$
Lean4
theorem tendsto_cons_iff {β : Type*} {f : List α → β} {b : Filter β} {a : α} {l : List α} :
Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p : α × List α => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b :=
by
have : 𝓝 (a :: l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1 :: p.2 :=
by
simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm, (Filter.seq_eq_filter_seq _ _).symm]
simp [-Filter.map_def, Function.comp_def, functor_norm]
rw [this, Filter.tendsto_map'_iff]; rfl
