theorem MeasureTheory.LocallyIntegrable.norm {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : Measure X} (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun (x : X) => ‖f x‖) μ