Prove2Me

lean_workbook_plus_77948

Proved

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

What about the function f(x,y)={y−x≤y≤x−yx≤y≤−xx−y≤x≤y−xy≤x≤−y f(x,y)=\begin{cases}y&-x\le y\le x\\-y&x\le y\le -x\\x&-y\le x\le y\\-x&y\le x\le -y\end{cases}?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77948 (x y : ℝ) (f : ℝ × ℝ → ℝ) (hf: f (x,y) = if (-x) ≤ y ∧ y ≤ x then y else if x ≤ y ∧ y ≤ (-x) then (-y) else if (-y) ≤ x ∧ x ≤ y then x else (-y)) : |f (x,y)| ≤ |x| + |y|   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph