Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ μ = 0
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ mass μ = 0 ↔ μ = 0
refine' ⟨fun μ_mass => _, fun hμ => by simp only [hμ, zero_mass]⟩
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ ↑μ = ↑0
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ μ = 0
apply toMeasure_injective
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ ↑↑↑μ univ = 0
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ ↑μ = ↑0
apply Measure.measure_univ_eq_zero.mp
no goals
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : mass μ = 0
⊢ ↑↑↑μ univ = 0
rwa [← ennreal_mass, ENNReal.coe_eq_zero]
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
hμ : μ = 0
⊢ mass μ = 0
simp only [hμ, zero_mass]