lean_workbook_plus_6002
Provedprove that given
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6002 : ∀ x y z : ℝ, x^2 + y^2 + z^2 = 1 → x + y + z ≤ Real.sqrt 3 := by sorry
Source
prove that given
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6002 : ∀ x y z : ℝ, x^2 + y^2 + z^2 = 1 → x + y + z ≤ Real.sqrt 3 := by sorry