Prove2Me

lean_workbook_plus_27813

Proved

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

Note that a2+b2+c2≥ab+bc+ca=1a^2+b^2+c^2 \ge ab+bc+ca=1 then a2+b2≥1−c2,b2+c2≥1−a2,c2+a2≥1−b2a^2+b^2 \ge 1-c^2, b^2+c^2\ge 1-a^2, c^2+a^2 \ge 1-b^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27813 (a b c: ℝ) (h : a * b + b * c + c * a = 1) :
  a * a + b * b ≥ 1 - c * c ∧ b * b + c * c ≥ 1 - a * a ∧ c * c + a * a ≥ 1 - b * b   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph