Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ ↑f)
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ ↑f)
refine' ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, _⟩
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (a : Ω), ↑(↑f a) ∂μ) < ⊤
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ ↑f)
simp only [HasFiniteIntegral, Function.comp_apply, NNReal.nnnorm_eq]
no goals
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (a : Ω), ↑(↑f a) ∂μ) < ⊤
exact lintegral_lt_top_of_boundedContinuous_to_nnreal _ f