no goals
α : Type u_1
β : Type ?u.101571
γ : Type ?u.101574
δ : Type u_2
δ' : Type ?u.101580
ι : Sort uι
s t u : Set α
π : δ → Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
g : α → (a : δ) → π a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a
simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
  MeasurableSpace.comap_comp, Function.comp, iSup_le_iff]