no goals
α : Type u_2
β✝ : Type ?u.39374
γ : Type ?u.39377
ι : Type ?u.39380
inst✝³ : Countable ι
f✝ g : α → β✝
inst✝² : TopologicalSpace β✝
β : Type u_1
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(approxBounded hf c n) x) atTop (𝓝 (f x))
filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx