measurableSet_of_differentiableAt

English

The set {x | DifferentiableAt 𝕜 f x} is measurable when the target space is complete.

Русский

Множество {x | DifferentiableAt 𝕜 f x} измеримо при завершенном пространстве мишени.

LaTeX

$$$$\text{MeasurableSet}\{x \mid \text{DifferentiableAt } 𝕜 f x\}.$$$$

Lean4

/-- The set of differentiability points of a function taking values in a complete space is
Borel-measurable. -/
theorem measurableSet_of_differentiableAt : MeasurableSet {x | DifferentiableAt 𝕜 f x} :=
  by
  have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
  convert measurableSet_of_differentiableAt_of_isComplete 𝕜 f this
  simp

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