α : Type u_1
β : Type u_2
γ : Type ?u.4342311
δ : Type ?u.4342314
ι : Type ?u.4342317
R : Type ?u.4342320
R' : Type ?u.4342323
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae μ ⊓ 𝓟 (sᶜ)] g
α : Type u_1
β : Type u_2
γ : Type ?u.4342311
δ : Type ?u.4342314
ι : Type ?u.4342317
R : Type ?u.4342320
R' : Type ?u.4342323
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae (Measure.restrict μ (sᶜ))] g
rw [ae_restrict_eq hs.compl]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4342311
δ : Type ?u.4342314
ι : Type ?u.4342317
R : Type ?u.4342320
R' : Type ?u.4342323
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae μ ⊓ 𝓟 (sᶜ)] g
exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right