Lean-Workbook Plus 21739: Continuity of the exponential function
ProvedWorkbookRestored.plus_21739lean-workbookrestored-importssource-checked
The real exponential function is continuous at every real point.
Source: Lean-Workbook row lean_workbook_plus_21739 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.
Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real
Formal statement
theorem WorkbookRestored.plus_21739 : ∀ x : ℝ, ContinuousAt (fun x => exp x) x := by sorry
Source