case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.11466
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑(μ + ν) x✝) = ((fun s => ENNReal.toNNReal (↑↑↑μ s)) + fun s => ENNReal.toNNReal (↑↑↑ν s)) x✝
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.11466
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ ν : FiniteMeasure Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑(μ + ν) s)) = (fun s => ENNReal.toNNReal (↑↑↑μ s)) + fun s => ENNReal.toNNReal (↑↑↑ν s)
funext
case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.11466
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ↑↑↑(μ + ν) x✝ = ↑↑↑μ x✝ + ↑↑↑ν x✝
case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.11466
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ENNReal.toNNReal (↑↑↑(μ + ν) x✝) = ((fun s => ENNReal.toNNReal (↑↑↑μ s)) + fun s => ENNReal.toNNReal (↑↑↑ν s)) x✝
simp [← ENNReal.coe_eq_coe]
no goals
case h
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.11466
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ↑↑↑(μ + ν) x✝ = ↑↑↑μ x✝ + ↑↑↑ν x✝
norm_cast