no goals
α : Type u_1
β : Type ?u.701577
γ : Type ?u.701580
δ : Type ?u.701583
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ HasFiniteIntegral f ↔ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) < ⊤
rw [HasFiniteIntegral, lintegral_nnnorm_eq_of_ae_nonneg h]