α : Type u_1
β : Type ?u.62355
m : MeasurableSpace α
μ ν✝ ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ rnDeriv (withDensity ν (indicator s 1)) ν =ᶠ[ae ν] indicator s 1
α : Type u_1
β : Type ?u.62355
m : MeasurableSpace α
μ ν✝ ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ rnDeriv (restrict ν s) ν =ᶠ[ae ν] indicator s 1
rw [← withDensity_indicator_one hs]
no goals
α : Type u_1
β : Type ?u.62355
m : MeasurableSpace α
μ ν✝ ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ rnDeriv (withDensity ν (indicator s 1)) ν =ᶠ[ae ν] indicator s 1
exact rnDeriv_withDensity _ (measurable_one.indicator hs)