case h
α : Type u_1
β : Type ?u.8097
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑(join 0) s = ↑↑0 s
α : Type u_1
β : Type ?u.8097
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ join 0 = 0
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.8097
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑(join 0) s = ↑↑0 s
simp only [hs, join_apply, lintegral_zero_measure, coe_zero, Pi.zero_apply]