theorem MeasureTheory.LocallyIntegrable.ofReal {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} {𝕜 : Type u_9} [RCLike 𝕜] {f : X → ℝ} (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun (x : X) => ↑(f x)) μ

theorem MeasureTheory.LocallyIntegrableOn.ofReal {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : Measure X} {s : Set X} {𝕜 : Type u_9} [RCLike 𝕜] {f : X → ℝ} (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (fun (x : X) => ↑(f x)) s μ