Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ 1 ≠ 0
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ toFiniteMeasure μ ≠ 0
rw [← FiniteMeasure.mass_nonzero_iff, μ.mass_toFiniteMeasure]
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ 1 ≠ 0
exact one_ne_zero