lean_workbook_plus_82011

Proved

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

Look at the fixed point of function , $x^2 -2 =x$ ... Fixed point is the point at which $f(x)=x$ . If we solve the equation $f(x)=x$ , with $f(x)=x^2-2$ . We get $x=-1$ or $x=2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82011  (x : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = x^2 - 2)
  (h₁ : f x = x) :
  x = -1 ∨ x = 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph