case nil
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
⊢ Tendsto prod (𝓝 []) (𝓝 (prod []))

case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (prod (x :: l)))
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
l : List α
⊢ Tendsto prod (𝓝 l) (𝓝 (prod l))
induction' l with x l ih
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (prod (x :: l)))
simp_rw [tendsto_cons_iff, prod_cons]
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : ContinuousAt (fun p => p.fst * p.snd) (x, prod l)
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : Tendsto (fun p => p.fst * p.snd) (𝓝 x ×ˢ 𝓝 (prod l)) (𝓝 ((x, prod l).fst * (x, prod l).snd))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : ContinuousAt (fun p => p.fst * p.snd) (x, prod l)
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
rw [ContinuousAt, nhds_prod_eq] at this
no goals
case cons
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 (prod l))
this : Tendsto (fun p => p.fst * p.snd) (𝓝 x ×ˢ 𝓝 (prod l)) (𝓝 ((x, prod l).fst * (x, prod l).snd))
⊢ Tendsto (fun p => p.fst * prod p.snd) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * prod l))
exact this.comp (tendsto_id.prod_map ih)
no goals
case nil
α : Type u_1
β : Type ?u.56124
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
⊢ Tendsto prod (𝓝 []) (𝓝 (prod []))
simp (config := { contextual := true }) [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]