lean_workbook_plus_10219

Proved

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

Prove that function $f(x) = x^{4} - 4x + 1$ is injective on the interval $[0,1]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10219 (f : ℝ → ℝ) (hf: f = fun x => x^4 - 4*x + 1) : ∀ x ∈ [0,1], ∀ y ∈ [0,1], f x = f y → x = y   :=  by sorry

Source