Differentiable_Function_is_Continuous

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

continuous-functionsdifferentiable-real-functionsproofwiki

Let $f$ be a real function defined on an interval $I$ . Let $x_0 \in I$ such that $f$ is differentiable at $x_0$ . Then $f$ is continuous at $x_0$ .

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic

theorem Differentiable_Function_is_Continuous (f : ℝ → ℝ) (x0 : ℝ) (hf : DifferentiableAt ℝ f x0) : ContinuousAt f x0 := by sorry

Source

https://proofwiki.org/wiki/Differentiable_Function_is_Continuous

View graph