lean_workbook_plus_16028
ProvedProve that given
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16028 (x y z: ℝ) (h : x + y + z = 1) : x ^ 2 + y ^ 2 + z ^ 2 ≥ 1 / 3 := by sorry
Source
Prove that given
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16028 (x y z: ℝ) (h : x + y + z = 1) : x ^ 2 + y ^ 2 + z ^ 2 ≥ 1 / 3 := by sorry