F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}
have : IsComplete (univ : Set F) := complete_univ
case h.e'_3.h.e'_2.h.a
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}
convert measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this
no goals
case h.e'_3.h.e'_2.h.a
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ
simp