case h
α : Type u_1
β : Type ?u.1757811
γ : Type ?u.1757814
δ : Type ?u.1757817
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity (μ + ν) f) s = ↑↑(withDensity μ f + withDensity ν f) s
α : Type u_1
β : Type ?u.1757811
γ : Type ?u.1757814
δ : Type ?u.1757817
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ withDensity (μ + ν) f = withDensity μ f + withDensity ν f
ext1 s hs
no goals
case h
α : Type u_1
β : Type ?u.1757811
γ : Type ?u.1757814
δ : Type ?u.1757817
m✝ : MeasurableSpace α
μ✝ ν✝ : Measure α
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity (μ + ν) f) s = ↑↑(withDensity μ f + withDensity ν f) s
simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]