Prove2Me

lean_workbook_plus_33290

Proved

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

Prove that ∣max⁡(a,b)−max⁡(c,d)∣≤max⁡(∣a−c∣,∣b−d∣)\left|\max\left(a,b\right)-\max\left(c,d\right)\right| \leq \max\left(\left|a-c\right|,\left|b-d\right|\right)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33290 (a b c d : ℝ) :
  |max a b - max c d| ≤ max (|a - c|) (|b - d|)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph