theorem
integrableOn_of_integrableOn_inter_support
{α : Type u_1}
{ε' : Type u_4}
[MeasurableSpace α]
{s : Set α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace.PseudoMetrizableSpace ε']
{f : α → ε'}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ∩ Function.support f) μ)
: