∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f (μ + ν) =
    (MeasureTheory.HasFiniteIntegral f μ ∧ MeasureTheory.HasFiniteIntegral f ν)