case h.e'_2.h.e'_3.h
α : Type u_1
β : Type ?u.925649
γ : Type ?u.925652
δ : Type ?u.925655
m : MeasurableSpace α
μ ν : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : ↑↑μ s = 0
⊢ Measure.restrict μ s = 0
α : Type u_1
β : Type ?u.925649
γ : Type ?u.925652
δ : Type ?u.925655
m : MeasurableSpace α
μ ν : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : ↑↑μ s = 0
⊢ (∫⁻ (x : α) in s, f x ∂μ) = 0
convert lintegral_zero_measure _
no goals
case h.e'_2.h.e'_3.h
α : Type u_1
β : Type ?u.925649
γ : Type ?u.925652
δ : Type ?u.925655
m : MeasurableSpace α
μ ν : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : ↑↑μ s = 0
⊢ Measure.restrict μ s = 0
exact Measure.restrict_eq_zero.2 hs'