lean_workbook_plus_7832

Proved

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

Let $h$ be a continuous bijective function defined from $R$ to $R$ such that $h(x) + h^{ - 1}(x) = 2x$ and there exists a real number $u$ such that $h(u)=u.$ Prove that $h(x) = x$ for every real number $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7832 (h : ℝ → ℝ) (h_bij : Function.Bijective h) (h_cont : Continuous h) (h_fixed : ∃ u, h u = u) (h_sum : ∀ x, h x + h⁻¹ x = 2 * x) : ∀ x, h x = x   :=  by sorry

Source

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

View graph