Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ (↑↑μ s)⁻¹ • ↑↑μ s = 1
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ ↑↑(μ[|s]) Set.univ = 1
rw [cond, Measure.smul_apply, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
no goals
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ (↑↑μ s)⁻¹ • ↑↑μ s = 1
exact ENNReal.inv_mul_cancel hcs (measure_ne_top _ s)