α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f a c x
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
⊢ Measurable (update f a)
refine measurable_pi_lambda _ fun x => ?_
case inl
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f x c x

case inr
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
hx : x ≠ a
⊢ Measurable fun c => update f a c x
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f a c x
rcases eq_or_ne x a with (rfl | hx)
no goals
case inl
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f x c x
simpa only [update_same] using measurable_id
no goals
case inr
α : Type ?u.103718
β : Type ?u.103721
γ : Type ?u.103724
δ : Type u_1
δ' : Type ?u.103730
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
hx : x ≠ a
⊢ Measurable fun c => update f a c x
simpa only [update_noteq hx] using measurable_const