Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.38918
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ ↑↑↑(restrict μ A) s = ↑↑↑μ (s ∩ A)
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.38918
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ (fun s => ENNReal.toNNReal (↑↑↑(restrict μ A) s)) s = (fun s => ENNReal.toNNReal (↑↑↑μ s)) (s ∩ A)
apply congr_arg ENNReal.toNNReal
no goals
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
R : Type ?u.38918
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ ↑↑↑(restrict μ A) s = ↑↑↑μ (s ∩ A)
exact Measure.restrict_apply s_mble