case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.10659
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑0 x✝) = OfNat.ofNat 0 x✝
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.10659
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
⊢ (fun s => ENNReal.toNNReal (↑↑↑0 s)) = 0
funext
no goals
case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.10659
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑0 x✝) = OfNat.ofNat 0 x✝
rfl