Prove2Me

lean_workbook_plus_34275

Proved

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

Let a≤b≤c a \leq b \leq c . Prove that: \n 3a≤a+b+c−a2+b2+c2−ab−bc−ca 3a \leq a + b + c - \sqrt {a^2 + b^2 + c^2 - ab - bc - ca}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34275 : ∀ a b c : ℝ, a ≤ b ∧ b ≤ c → 3 * a ≤ a + b + c - Real.sqrt (a ^ 2 + b ^ 2 + c ^ 2 - a * b - b * c - c * a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph