no goals
α : Type u_1
β : Type u_2
γ : Type ?u.700144
δ : Type ?u.700147
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ HasFiniteIntegral f ↔ (∫⁻ (a : α), edist (f a) 0 ∂μ) < ⊤
simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]