differentiableOn_integral_of_continuous

English

If f is continuous, then the map u ↦ ∫_{a}^{u} f(x) dx is differentiable on any real set s; its derivative is f(u) on s.

Русский

Если f непрерывна, то отображение u ↦ ∫_{a}^{u} f(x) dx дифференцируемо на любом множестве s; производной является f(u) на s.

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{R}}\\bigl(\\lambda u: \\int_{a}^{u} f(x)\\,dx\\bigr)(s)\\;\\text{ с } f(u)\\text{ как производной на } s.$$$

Lean4

/-- The integral of a continuous function is differentiable on a real set `s`. -/
theorem differentiableOn_integral_of_continuous {s : Set ℝ} (hcont : Continuous f) :
    DifferentiableOn ℝ (fun u => ∫ x in a..u, f x) s :=
  (differentiable_integral_of_continuous hcont).differentiableOn

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