α : Type u_2
β : Type ?u.277142
γ : Type ?u.277145
δ : Type ?u.277148
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
f : ι → α → ℝ≥0∞
⊢ (⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ) ≤ ∫⁻ (a : α), iSup (fun i => f i) a ∂μ
α : Type u_2
β : Type ?u.277142
γ : Type ?u.277145
δ : Type ?u.277148
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
f : ι → α → ℝ≥0∞
⊢ (⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ) ≤ ∫⁻ (a : α), ⨆ (i : ι), f i a ∂μ
simp only [← iSup_apply]
no goals
α : Type u_2
β : Type ?u.277142
γ : Type ?u.277145
δ : Type ?u.277148
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
f : ι → α → ℝ≥0∞
⊢ (⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ) ≤ ∫⁻ (a : α), iSup (fun i => f i) a ∂μ
exact (monotone_lintegral μ).le_map_iSup