Prove2Me

lean_workbook_plus_13848

Proved

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

Find the minimum value of the function : 1)y=∣x−3∣+∣x∣+∣x+3∣+∣x+5∣1) y=\lvert{x-3}\rvert+\lvert{x}\rvert+\lvert{x+3}\rvert+\lvert{x}+5\rvert 2)y=∣x2+3x+1∣+∣x2−1∣+∣3x−2∣2)y=\lvert{x^2+3x+1}\rvert+\lvert{x^2-1}\rvert+\lvert{3x-2}\rvert .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13848 (x : ℝ) : 11 ≤ abs (x - 3) + abs x + abs (x + 3) + abs (x + 5)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph