case h.e'_3.h.e'_4.h
α : Type u_3
β : Type ?u.284610
γ : Type ?u.284613
δ : Type ?u.284616
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ (⨅ (i : ι) (h : ι' i), f i h a) = iInf (fun i => ⨅ (j : ι' i), f i j) a
α : Type u_3
β : Type ?u.284610
γ : Type ?u.284613
δ : Type ?u.284616
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ (∫⁻ (a : α), ⨅ (i : ι) (h : ι' i), f i h a ∂μ) ≤ ⨅ (i : ι) (h : ι' i), ∫⁻ (a : α), f i h a ∂μ
convert(monotone_lintegral μ).map_iInf₂_le f with a
no goals
case h.e'_3.h.e'_4.h
α : Type u_3
β : Type ?u.284610
γ : Type ?u.284613
δ : Type ?u.284616
m : MeasurableSpace α
μ ν : Measure α
ι : Sort u_1
ι' : ι → Sort u_2
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ (⨅ (i : ι) (h : ι' i), f i h a) = iInf (fun i => ⨅ (j : ι' i), f i j) a
simp only [iInf_apply]