α : Type u_2
β : Type u_1
γ : Type ?u.832965
δ : Type ?u.832968
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
this : AEStronglyMeasurable (fun x => c) μ
⊢ (Integrable fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.832965
δ : Type ?u.832968
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
⊢ (Integrable fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.832965
δ : Type ?u.832968
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
this : AEStronglyMeasurable (fun x => c) μ
⊢ (Integrable fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff]