Prove2Me

lean_workbook_plus_130

Proved

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

f(x)={0, 0≤x≤13x−13,13<x≤1f(x) = \left\{\begin{aligned} &0 &&, \: 0 \le x \le \frac{1}{3}\\ &x-\frac{1}{3} &&, \frac{1}{3} < x \le 1 \end{aligned} \right.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_130 (x : ℝ) (f : ℝ → ℝ) (hf: f x = if x ∈ Set.Icc 0 (1/3) then 0 else x - 1/3) : f x = if x ∈ Set.Icc 0 (1/3) then 0 else x - 1/3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph