English
Let f: α → E → F be such that f is continuous after currying. Then the set of points (p, t) with p ∈ α and t ∈ E at which f(p, ·) is differentiable at t is a measurable subset of α × E.
Русский
Пусть f: α → E → F таково, что отображение сглажено непрерывно после каррирования. Тогда множество точек (p, t) ∈ α × E, для которых отображение f(p, ·) дифференцируемо в t, является измеримым подмножество α × E.
LaTeX
$$$$\\MeasurableSet \\{ p \\in \\alpha \\times E \\mid \\DifferentiableAt 𝕜 (f\\,p.1) p.2 \\}.$$$$
Lean4
/-- The set of differentiability points of a continuous function depending on a parameter taking
values in a complete space is Borel-measurable. -/
theorem measurableSet_of_differentiableAt_with_param (hf : Continuous f.uncurry) :
MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2} :=
by
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
convert measurableSet_of_differentiableAt_of_isComplete_with_param hf this
simp
