α : Type u_1
β : Type u_2
γ : Type ?u.1305559
δ : Type ?u.1305562
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) ≠ ⊤
α : Type u_1
β : Type u_2
γ : Type ?u.1305559
δ : Type ?u.1305562
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ↑‖↑↑f x‖₊ ∂μ
rw [norm_def, ENNReal.ofReal_toReal]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1305559
δ : Type ?u.1305562
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ) ≠ ⊤
exact ne_of_lt (hasFiniteIntegral_coeFn f)