α : Type u_1
β : Type ?u.76135
γ : Type ?u.76138
δ : Type ?u.76141
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * ↑↑(Measure.restrict μ s) univ < ⊤
α : Type u_1
β : Type ?u.76135
γ : Type ?u.76138
δ : Type ?u.76141
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ (∫⁻ (x : α) in s, c ∂μ) < ⊤
rw [lintegral_const]
no goals
α : Type u_1
β : Type ?u.76135
γ : Type ?u.76138
δ : Type ?u.76141
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * ↑↑(Measure.restrict μ s) univ < ⊤
exact ENNReal.mul_lt_top hc (measure_ne_top (μ.restrict s) univ)