no goals
α : Type u_2
β : Type u_3
γ : Type ?u.841691
δ : Type ?u.841694
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ι : Type u_1
m : MeasurableSpace α
f : α → β
μ : ι → Measure α
s : Finset ι
⊢ Integrable f ↔ ∀ (i : ι), i ∈ s → Integrable f
induction s using Finset.induction_on <;> simp [*]