measurableSet_of_differentiableWithinAt_Ioi

English

The set of x such that DifferentiableAt 𝕜 (f x.1) x.2 and fderiv 𝕜 (f x.1) x.2 ∈ K is measurable, when K is complete.

Русский

Множество точек x, для которых выполняются дифференцируемость и принадлежность производной K, измеримо при условии полноты K.

LaTeX

$$$\\text{MeasurableSet}\\{p: \\alpha \\times E \\mid ( DifferentiableAt 𝕜 (f p.1) p.2) \\land (fderiv 𝕜 (f p.1) p.2) \\in K\\}$ (при изначальном hf и hK).$$

Lean4

/-- The set of right differentiability points of a function taking values in a complete space is
Borel-measurable. -/
theorem measurableSet_of_differentiableWithinAt_Ioi : MeasurableSet {x | DifferentiableWithinAt ℝ f (Ioi x) x} := by
  simpa [differentiableWithinAt_Ioi_iff_Ici] using measurableSet_of_differentiableWithinAt_Ici f

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