diffContOnCl — Mathlib

English

If f is differentiable on a set, then the derivative is continuous on that set’s closure.

Русский

Если функция дифференцируема на множестве, то производная непрерывна на замыкании этого множества.

LaTeX

$$$$\\text{If } f\\text{ is differentiable on } s,\\text{ then } (\\mathrm{d}f)\\text{ is continuous on } \\overline{s}. $$$$

Lean4

theorem diffContOnCl (h : Differentiable 𝕜 f) : DiffContOnCl 𝕜 f s :=
  ⟨h.differentiableOn, h.continuous.continuousOn⟩

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