case h.e'_4.h.e'_4.h
α : Type u_3
β : Type ?u.277932
γ : Type ?u.277935
δ : Type ?u.277938
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ (⨆ (i : ι) (j : ι' i), f i j a) = iSup (fun i => ⨆ (j : ι' i), f i j) a
α : Type u_3
β : Type ?u.277932
γ : Type ?u.277935
δ : Type ?u.277938
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ (⨆ (i : ι) (j : ι' i), ∫⁻ (a : α), f i j a ∂μ) ≤ ∫⁻ (a : α), ⨆ (i : ι) (j : ι' i), f i j a ∂μ
convert (monotone_lintegral μ).le_map_iSup₂ f with a
no goals
case h.e'_4.h.e'_4.h
α : Type u_3
β : Type ?u.277932
γ : Type ?u.277935
δ : Type ?u.277938
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ (⨆ (i : ι) (j : ι' i), f i j a) = iSup (fun i => ⨆ (j : ι' i), f i j) a
simp only [iSup_apply]