no goals
α : Type u_1
β : Type ?u.1495663
E : Type u_2
F : Type ?u.1495669
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
C : E
⊢ C = 0 ∨ ↑↑(Measure.restrict μ s) univ < ⊤ ↔ C = 0 ∨ ↑↑μ s < ⊤
rw [Measure.restrict_apply_univ]