no goals
ι : Type ?u.11347958
𝕜 : Type ?u.11347961
E : Type u_1
F : Type ?u.11347967
A : Type ?u.11347970
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
h : a ≤ b
hf : ¬AEStronglyMeasurable f (Measure.restrict μ (Ioc a b))
⊢ ¬AEStronglyMeasurable (fun x => f x) (Measure.restrict μ (Ι a b))
rwa [uIoc_of_le h]