𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
case h.e'_3.h.e'_2.h.a
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : E
⊢ DifferentiableAt 𝕜 f x✝ ↔ DifferentiableAt 𝕜 f x✝ ∧ fderiv 𝕜 f x✝ ∈ univ
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableAt 𝕜 f x}
convert measurableSet_of_differentiableAt_of_isComplete 𝕜 f this
no goals
case h.e'_3.h.e'_2.h.a
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : E
⊢ DifferentiableAt 𝕜 f x✝ ↔ DifferentiableAt 𝕜 f x✝ ∧ fderiv 𝕜 f x✝ ∈ univ
simp