measurableSet_of_differentiableWithinAt_Ici

English

If K is complete, then D f K is included in the set of x with differentiability and derivative in K.

Русский

Если K полное, то D f K ⊆ {x | DifferentiableWithinAt …}.

LaTeX

$$D f K ⊆ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}$$

Lean4

/-- The set of right differentiability points of a function taking values in a complete space is
Borel-measurable. -/
theorem measurableSet_of_differentiableWithinAt_Ici : MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x} :=
  by
  have : IsComplete (univ : Set F) := complete_univ
  convert measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this
  simp

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