α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
rw [this, Filter.tendsto_map'_iff]
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
dsimp
no goals
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.fst :: p.snd)) (𝓝 a ×ˢ 𝓝 l) b
rfl
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
⊢ (Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l) = (fun p => p.fst :: p.snd) <$> Seq.seq (Prod.mk <$> 𝓝 a) fun x => 𝓝 l
α : Type u_2
β✝ : Type ?u.5720
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β✝
β : Type u_1
f : List α → β
b : Filter β
a : α
l : List α
⊢ 𝓝 (a :: l) = Filter.map (fun p => p.fst :: p.snd) (𝓝 a ×ˢ 𝓝 l)
simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
  (Filter.seq_eq_filter_seq _ _).symm]