Prove2Me

lean_workbook_plus_21854

Disproved

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

Prove that there does not exist the function f:R→Rf:\mathbb {R} \rightarrow \mathbb {R} such that f(0)=0f(0)=0 and f(x+y)≥f(x)+yf(f(x)),∀x,y∈Rf(x+y) \geq f(x)+yf(f(x)), \forall x, y \in \mathbb{R} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21854    (f : ℝ → ℝ)
    (h₀ : f 0 = 0)
    (h₁ : ∀ x y, f (x + y) ≥ f x + y * f (f x)) :
    False   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph