Prove2Me

lean_workbook_plus_64367

Proved

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

Given a function ff such that f(x)≤x∀x∈Rf(x)\le x\forall x\in\mathbb{R} and f(x+y)≤f(x)+f(y)∀{x,y}∈Rf(x+y)\le f(x)+f(y)\forall \{x,y\}\in\mathbb{R} , prove that f(x)=x∀x∈Rf(x)=x\forall x\in\mathbb{R} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64367    (f : ℝ → ℝ)
    (h₁ : ∀ x, f x ≤ x)
    (h₂ : ∀ 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