case intro
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1516393
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), IntegrableOn f (t i)
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1516393
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
inst✝ : Finite β
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), IntegrableOn f (t i)
cases nonempty_fintype β
no goals
case intro
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1516393
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), IntegrableOn f (t i)
simpa using @integrableOn_finset_iUnion _ _ _ _ _ f μ Finset.univ t