lean_workbook_plus_5108
ProvedFrom we have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5108 (a b c : ℝ) (h : a^2 + b^2 + c^2 = 1) : a^2 <= 1 ∧ b^2 <= 1 ∧ c^2 <= 1 := by sorry
Source
From we have .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5108 (a b c : ℝ) (h : a^2 + b^2 + c^2 = 1) : a^2 <= 1 ∧ b^2 <= 1 ∧ c^2 <= 1 := by sorry