Prove2Me

Linear_Function_is_Continuous

Proved

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

continuous-functionslinear-function-is-continuousproofwiki

Let α,β∈R\alpha, \beta \in \R be real numbers. Let f:R→Rf : \R \to \R be the real function with \mapfx=αx+β\map f x = \alpha x + \beta for all x∈Rx \in \R. Then ff is continuous at every real number c∈Rc \in \R.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic

theorem Linear_Function_is_Continuous (alpha beta : ℝ) : Continuous (fun x : ℝ => alpha * x + beta) := by sorry
Source
https://proofwiki.org/wiki/Linear_Function_is_Continuous

View graph