lean_workbook_plus_49617
ProvedIf need to prove:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49617 (a b c : ℝ) (h : c = 0) : 2 + (1 / 4) * ((a - b) ^ 2 + a ^ 2 + b ^ 2) ≥ a + b := by sorry
Source
If need to prove:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49617 (a b c : ℝ) (h : c = 0) : 2 + (1 / 4) * ((a - b) ^ 2 + a ^ 2 + b ^ 2) ≥ a + b := by sorry