no goals
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.41322
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : FiniteMeasure Ω
A : Set Ω
⊢ restrict μ A ≠ 0 ↔ (fun s => ENNReal.toNNReal (↑↑↑μ s)) A ≠ 0
rw [← mass_nonzero_iff, restrict_mass]