no goals
ι : Type u_2
α : Type u_1
X : Type ?u.169976
M : Type u_3
N : Type ?u.169982
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
x✝ : ∀ (i : ι), i ∈ [] → Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f c b) [])) x (𝓝 (List.prod (List.map a [])))
simp [tendsto_const_nhds]
ι : Type u_2
α : Type u_1
X : Type ?u.169976
M : Type u_3
N : Type ?u.169982
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * List.prod (List.map (fun c => f✝ c b) l)) x (𝓝 (a f * List.prod (List.map a l)))
ι : Type u_2
α : Type u_1
X : Type ?u.169976
M : Type u_3
N : Type ?u.169982
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f✝ c b) (f :: l))) x (𝓝 (List.prod (List.map a (f :: l))))
simp only [List.map_cons, List.prod_cons]
no goals
ι : Type u_2
α : Type u_1
X : Type ?u.169976
M : Type u_3
N : Type ?u.169982
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * List.prod (List.map (fun c => f✝ c b) l)) x (𝓝 (a f * List.prod (List.map a l)))
exact
  (h f (List.mem_cons_self _ _)).mul
    (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))