Prove2Me

lean_workbook_plus_44571

Disproved

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

a) f:R→Rf : \mathbb{R} \rightarrow \mathbb{R} so that ∣f(x)−f(y)∣>1,∀x,y∈R\mid f(x) - f(y) \mid > 1, \forall x, y \in \mathbb{R}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44571 (f : ℝ → ℝ): (∀ x y :ℝ, abs (f x - f y) > 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph