α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.69940
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ↑((fun n => SimpleFunc.pair (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 ((fun x => (f x, g x)) x))
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.69940
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable fun x => (f x, g x)
refine' ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => _⟩
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.69940
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ↑((fun n => SimpleFunc.pair (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (f x) ×ˢ 𝓝 (g x))
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.69940
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ↑((fun n => SimpleFunc.pair (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 ((fun x => (f x, g x)) x))
rw [nhds_prod_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.69940
inst✝² : Countable ι
f✝ g✝ : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ↑((fun n => SimpleFunc.pair (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (f x) ×ˢ 𝓝 (g x))
exact Tendsto.prod_mk (hf.tendsto_approx x) (hg.tendsto_approx x)