Finitely strongly measurable functions with value in ENNReal

A measurable function with finite Lebesgue integral can be approximated by simple functions whose support has finite measure.

theorem ENNReal.finStronglyMeasurable_of_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hf_meas : Measurable f) : MeasureTheory.FinStronglyMeasurable f μ

theorem ENNReal.aefinStronglyMeasurable_of_aemeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hf_meas : AEMeasurable f μ) : MeasureTheory.AEFinStronglyMeasurable f μ