no goals
α : Type u_2
β : Type ?u.710602
γ : Type ?u.710605
γ₂ : Type ?u.710608
δ : Type u_1
ι : Sort y
s t u : Set α
inst✝¹⁷ : TopologicalSpace α
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : OpensMeasurableSpace α
inst✝¹⁴ : TopologicalSpace β
inst✝¹³ : MeasurableSpace β
inst✝¹² : OpensMeasurableSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace γ
inst✝⁹ : BorelSpace γ
inst✝⁸ : TopologicalSpace γ₂
inst✝⁷ : MeasurableSpace γ₂
inst✝⁶ : BorelSpace γ₂
inst✝⁵ : MeasurableSpace δ
α' : Type ?u.710704
inst✝⁴ : TopologicalSpace α'
inst✝³ : MeasurableSpace α'
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
a b : α
inst✝ : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a => Max.max (f a) (g a)
simpa only [max_def'] using hf.piecewise (measurableSet_le hg hf) hg