no goals
α : Type u_1
β : Type u_2
γ : Type ?u.708905
δ : Type ?u.708908
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
c : β
⊢ (HasFiniteIntegral fun x => c) ↔ c = 0 ∨ ↑↑μ univ < ⊤
simp [HasFiniteIntegral, lintegral_const, lt_top_iff_ne_top, ENNReal.mul_eq_top,
  or_iff_not_imp_left]