no goals
α : Type u_2
β✝ : Type ?u.10411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 []) (r [])
rwa [nhds_nil]
α : Type u_2
β✝ : Type ?u.10411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
α : Type u_2
β✝ : Type ?u.10411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))
rw [tendsto_cons_iff]
no goals
α : Type u_2
β✝ : Type ?u.10411
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
exact h_cons l a (@tendsto_nhds _ _ _ h_nil h_cons l)