α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Measurable fun x => ↑(g x)
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ Measurable g
simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf⊢
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Tendsto (fun i x => ↑(f i x)) u (𝓝 fun x => ↑(g x))
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Measurable fun x => ↑(g x)
refine' measurable_of_tendsto_ennreal' u hf _
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ ∀ (x : α), Tendsto (fun i => ↑(f i x)) u (𝓝 ↑(g x))
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ Tendsto (fun i x => ↑(f i x)) u (𝓝 fun x => ↑(g x))
rw [tendsto_pi_nhds] at lim⊢
no goals
α : Type u_2
β : Type ?u.2014
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_1
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable fun x => ↑(f i x)
⊢ ∀ (x : α), Tendsto (fun i => ↑(f i x)) u (𝓝 ↑(g x))
exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)