𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ MeasurableSet (fderiv 𝕜 f ⁻¹' s)
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
⊢ Measurable (fderiv 𝕜 f)
refine' measurable_of_isClosed fun s hs => _
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet (fderiv 𝕜 f ⁻¹' s)
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ MeasurableSet (fderiv 𝕜 f ⁻¹' s)
have :
  fderiv 𝕜 f ⁻¹' s =
    { x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s } ∪
      { x | ¬DifferentiableAt 𝕜 f x } ∩ { _x | (0 : E →L[𝕜] F) ∈ s } :=
  Set.ext fun x => mem_preimage.trans fderiv_mem_iff
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet ({x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s})
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet (fderiv 𝕜 f ⁻¹' s)
rw [this]
no goals
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet ({x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s})
exact
  (measurableSet_of_differentiableAt_of_isComplete _ _ hs.isComplete).union
    ((measurableSet_of_differentiableAt _ _).compl.inter (MeasurableSet.const _))