continuousOn — Mathlib

English

If HasDerivAt f at every point of s with some derivatives f'(x), then f is continuous on s.

Русский

Если для каждой точки x из s существует производная f'(x) = f′ у f, то f непрерывна на s.

LaTeX

$$$\\forall x \\in s,\\ HasDerivAt f (f'(x)) x \\Rightarrow \\text{ContinuousOn } f\\ s$$$

Lean4

protected theorem continuousOn {f f' : 𝕜 → F} (hderiv : ∀ x ∈ s, HasDerivAt f (f' x) x) : ContinuousOn f s :=
  fun x hx => (hderiv x hx).continuousAt.continuousWithinAt

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