lean_workbook_plus_73216
ProvedThe ineq is equivalent to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73216 (a b c : ℝ) : (a - b) ^ 2 + (a - c) ^ 2 ≥ 1 / 2 * (b - c) ^ 2 := by sorry
Source
The ineq is equivalent to .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_73216 (a b c : ℝ) : (a - b) ^ 2 + (a - c) ^ 2 ≥ 1 / 2 * (b - c) ^ 2 := by sorry