Prove2Me

lean_workbook_plus_10900

Proved

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

Given f(x)={2x if x<0.52−2x if x≥0.5f(x)=\begin{cases}2x\text{ if }x<0.5\\2-2x\text{ if }x\geq 0.5\end{cases}, does f([0,1])⊂[0,1]f([0,1]) \subset [0,1] hold?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10900 (f : ℝ → ℝ) (f_of : ∀ x < 0.5, f x = 2 * x) (f_on : ∀ x ≥ 0.5, f x = 2 - 2 * x) : ∀ x ∈ Set.Icc 0 1, f x ∈ Set.Icc 0 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph