α : Type u_1
β : Type ?u.38581
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ (∫⁻ (x : α) in univ, rnDeriv μ ν x ∂ν) < ⊤
α : Type u_1
β : Type ?u.38581
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ (∫⁻ (x : α), rnDeriv μ ν x ∂ν) < ⊤
rw [← set_lintegral_univ]
no goals
α : Type u_1
β : Type ?u.38581
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ (∫⁻ (x : α) in univ, rnDeriv μ ν x ∂ν) < ⊤
exact lintegral_rnDeriv_lt_top_of_measure_ne_top _ (measure_lt_top _ _).ne