measurableSet_lineDifferentiableAt

English

If f is continuous, then the set of points x for which lineDifferentiableAt 𝕜 f x v holds is a measurable subset of E.

Русский

Если f непрерывна, то множество точек x, для которых lineDifferentiableAt 𝕜 f x v выполняется, измеримо в E.

LaTeX

$$$$ \text{MeasurableSet} \{x \in E : LineDifferentiableAt 𝕜 f x v\} $$$$

Lean4

theorem measurableSet_lineDifferentiableAt (hf : Continuous f) : MeasurableSet {x : E | LineDifferentiableAt 𝕜 f x v} :=
  by
  borelize 𝕜
  let g : E → 𝕜 → F := fun x t ↦ f (x + t • v)
  have hg : Continuous g.uncurry := by fun_prop
  exact measurable_prodMk_right (measurableSet_of_differentiableAt_with_param 𝕜 hg)

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