α : Type u_1
β : Type ?u.4553
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Filter.seq (Filter.map (fun a b => (a, b).fst :: (a, b).snd) (𝓝 a)) (𝓝 l) ≤ Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l
α : Type u_1
β : Type ?u.4553
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))
rw [nhds_cons, Tendsto, Filter.map_prod]
no goals
α : Type u_1
β : Type ?u.4553
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Filter.seq (Filter.map (fun a b => (a, b).fst :: (a, b).snd) (𝓝 a)) (𝓝 l) ≤ Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l
exact le_rfl