α : Type u_1
β : Type ?u.734418
γ : Type ?u.734421
δ : Type ?u.734424
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hfi : HasFiniteIntegral f
x : α
⊢ ENNReal.ofReal (f x) ≤ ↑‖f x‖₊
α : Type u_1
β : Type ?u.734418
γ : Type ?u.734421
δ : Type ?u.734424
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hfi : HasFiniteIntegral f
⊢ IsFiniteMeasure (Measure.withDensity μ fun x => ENNReal.ofReal (f x))
refine' isFiniteMeasure_withDensity ((lintegral_mono fun x => _).trans_lt hfi).ne
no goals
α : Type u_1
β : Type ?u.734418
γ : Type ?u.734421
δ : Type ?u.734424
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hfi : HasFiniteIntegral f
x : α
⊢ ENNReal.ofReal (f x) ≤ ↑‖f x‖₊
exact Real.ofReal_le_ennnorm (f x)