lean_workbook_plus_75315

Disproved

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

b) $f : \mathbb{Q} \rightarrow \mathbb{Q}$ so that $\mid f(x) - f(y) \mid > 1, \forall x, y \in \mathbb{Q}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75315 : ∃ f : ℚ → ℚ, ∀ x y : ℚ, abs (f x - f y) > 1   :=  by sorry

Source