Prove2Me

lean_workbook_plus_41094

Proved

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

x2+y22≥x+y2 \sqrt{\frac{x^2+y^2}{2}}\ge\frac{x+y}{2} ; y2+z22≥y+z2 \sqrt{\frac{y^2+z^2}{2}}\ge\frac{y+z}{2} , z2+x22≥z+x2 \sqrt{\frac{z^2+x^2}{2}}\ge\frac{z+x}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_41094 (x y z : ℝ) : (Real.sqrt ((x ^ 2 + y ^ 2) / 2) ≥ (x + y) / 2 ∧ Real.sqrt ((y ^ 2 + z ^ 2) / 2) ≥ (y + z) / 2 ∧ Real.sqrt ((z ^ 2 + x ^ 2) / 2) ≥ (z + x) / 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph