Prove2Me

lean_workbook_plus_29115

Proved

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

What are your thoughts about?

f(x)={x[0,1] x−2(1,2]f(x) = \begin{cases} x & [0, 1] \ x - 2 & (1, 2] \end{cases}

and

g(x)={−x[0,1] −x+2(1,2]g(x) = \begin{cases} -x & [0, 1] \ -x + 2 & (1, 2] \end{cases}

Thus,

f(x)+g(x)={0[0,1] 0(1,2]f(x) + g(x) = \begin{cases} 0 & [0, 1] \ 0 & (1, 2] \end{cases}

As a result, the sum has a limit.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29115  (f g : ℝ → ℝ)
  (h₀ : ∀ x, 0 ≤ x ∧ x ≤ 1 → f x = x)
  (h₁ : ∀ x, 1 < x ∧ x ≤ 2 → f x = x - 2)
  (h₂ : ∀ x, 0 ≤ x ∧ x ≤ 1 → g x = -x)
  (h₃ : ∀ x, 1 < x ∧ x ≤ 2 → g x = -x + 2) :
  ∀ x, 0 ≤ x ∧ x ≤ 2 → f x + g x = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph