lean_workbook_plus_49564
Provedand
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49564 (a b c : ℝ) : a^2 + b^2 + c^2 + 3 ≥ 2 * (a + b + c) ↔ (a - 1)^2 + (b - 1)^2 + (c - 1)^2 ≥ 0 := by sorry
Source
and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49564 (a b c : ℝ) : a^2 + b^2 + c^2 + 3 ≥ 2 * (a + b + c) ↔ (a - 1)^2 + (b - 1)^2 + (c - 1)^2 ≥ 0 := by sorry