α : Type u_1
β : Type u_2
γ : Type ?u.4290136
δ : Type ?u.4290139
ι : Type ?u.4290142
R : Type ?u.4290145
R' : Type ?u.4290148
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae μ ⊓ 𝓟 s] f
α : Type u_1
β : Type u_2
γ : Type ?u.4290136
δ : Type ?u.4290139
ι : Type ?u.4290142
R : Type ?u.4290145
R' : Type ?u.4290148
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae (Measure.restrict μ s)] f
rw [ae_restrict_eq hs]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4290136
δ : Type ?u.4290139
ι : Type ?u.4290142
R : Type ?u.4290145
R' : Type ?u.4290148
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f g : α → β
hs : MeasurableSet s
⊢ piecewise s f g =ᶠ[ae μ ⊓ 𝓟 s] f
exact (piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right