Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ ENNReal.toReal (∫⁻ (x : Ω), ↑(↑f x) ∂μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal ↑(↑f a) ∂μ)

Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ 0 ≤ᵐ[μ] fun x => ↑(↑f x)
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ ENNReal.toReal (∫⁻ (x : Ω), ↑(↑f x) ∂μ) = ∫ (x : Ω), ↑(↑f x) ∂μ
rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using
      (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]
no goals
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ AEStronglyMeasurable (fun x => ↑(↑f x)) μ
simpa [Function.comp_apply] using
(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable
no goals
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ ENNReal.toReal (∫⁻ (x : Ω), ↑(↑f x) ∂μ) = ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal ↑(↑f a) ∂μ)
simp only [ENNReal.ofReal_coe_nnreal]
case hp
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ ∀ (x : Ω), OfNat.ofNat 0 x ≤ (fun x => ↑(↑f x)) x
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ 0 ≤ᵐ[μ] fun x => ↑(↑f x)
apply eventually_of_forall
no goals
case hp
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
μ : Measure Ω
⊢ ∀ (x : Ω), OfNat.ofNat 0 x ≤ (fun x => ↑(↑f x)) x
simp only [Pi.zero_apply, NNReal.zero_le_coe, imp_true_iff]