measurableSet_of_differentiableAt_of_isComplete

English

The set of differentiability points with derivative in a complete set is a Borel-measurable set.

Русский

Множество точек дифференцируемости с производной в полном множестве является бореллевым.

LaTeX

$$$$\text{MeasurableSet}\{x \mid \text{DifferentiableAt } 𝕜 f x \wedge fderiv 𝕜 f x \in K\}.$$$$

Lean4

/-- The set of differentiability points of a function, with derivative in a given complete set,
is Borel-measurable. -/
theorem measurableSet_of_differentiableAt_of_isComplete {K : Set (E →L[𝕜] F)} (hK : IsComplete K) :
    MeasurableSet {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} :=
  by
  simp only [D, differentiable_set_eq_D K hK]
  aesop (add safe apply [MeasurableSet.iUnion, MeasurableSet.iInter, isOpen_B]) (add unsafe IsOpen.measurableSet)

Похожие утверждения