no goals
α : Type u_1
β : Type ?u.925342
γ : Type ?u.925345
δ : Type ?u.925348
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (∫⁻ (x : α) in ∅, f x ∂μ) = 0
rw [Measure.restrict_empty, lintegral_zero_measure]