case h.e'_3.h.e'_3.h.e'_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.19449
δ : Type ?u.19452
ι : Type ?u.19455
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
α : Type u_2
β : Type u_1
γ : Type ?u.19449
δ : Type ?u.19452
ι : Type ?u.19455
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β), f b) ≤ ∑ p : β, ↑↑μ (f p)
convert measure_biUnion_finset_le Finset.univ f
no goals
case h.e'_3.h.e'_3.h.e'_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.19449
δ : Type ?u.19452
ι : Type ?u.19455
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
simp