lean_workbook_plus_80805

Proved

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

Show that $f(x)=x$ for every real number $x$ given the following inequalities for every pair of real numbers $x,y$ : $f(x)\leq x$ and $f(x+y)\leq f(x)+f(y)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80805 (f : ℝ → ℝ) (hf: ∀ x, f x ≤ x) (hadd: ∀ x y, f (x + y) ≤ f x + f y) : ∀ x, f x = x   :=  by sorry

Source

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

View graph