ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a => List.prod (List.map (fun i => f i a) l)) t x
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
⊢ ContinuousOn (fun a => List.prod (List.map (fun i => f i a) l)) t
intro x hx
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt (restrict t fun a => List.prod (List.map (fun i => f i a) l)) { val := x, property := hx }
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a => List.prod (List.map (fun i => f i a) l)) t x
rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt (restrict t fun a => List.prod (List.map (fun i => f i a) l)) { val := x, property := hx }
refine' tendsto_list_prod _ fun i hi => _
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
specialize h i hi x hx
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (restrict t (f i)) { val := x, property := hx }
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h
no goals
ι : Type u_1
α : Type ?u.175300
X : Type u_2
M : Type u_3
N : Type ?u.175309
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (restrict t (f i)) { val := x, property := hx }
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
exact h