English
The set {x | DifferentiableAt 𝕜 f x} is measurable when the codomain is complete.
Русский
Множество {x | DifferentiableAt 𝕜 f x} измеримо, если целое пространство полно.
LaTeX
$$$$\text{MeasurableSet}\{x \mid \text{DifferentiableAt } 𝕜 f x\}.$$$$
Lean4
@[measurability, fun_prop]
theorem measurable_fderiv : Measurable (fderiv 𝕜 f) :=
by
refine measurable_of_isClosed fun s hs => ?_
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
rw [this]
exact
(measurableSet_of_differentiableAt_of_isComplete _ _ hs.isComplete).union
((measurableSet_of_differentiableAt _ _).compl.inter (MeasurableSet.const _))
