α : Type u_2
β : Type u_1
γ : Type ?u.1026302
δ : Type ?u.1026305
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ) ≤ ∫⁻ (a : α), f a ∂sum fun i => Measure.restrict μ (s i)
α : Type u_2
β : Type u_1
γ : Type ?u.1026302
δ : Type ?u.1026305
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ) ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
rw [← lintegral_sum_measure]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1026302
δ : Type ?u.1026305
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ) ≤ ∫⁻ (a : α), f a ∂sum fun i => Measure.restrict μ (s i)
exact lintegral_mono' restrict_iUnion_le le_rfl