lean_workbook_plus_61599
Proved(Proof) For all we have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61599 (x y z : ℝ) : (x - z) ^ 2 ≤ 2 * ((x - y) ^ 2 + (y - z) ^ 2) := by sorry
Source
(Proof) For all we have .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61599 (x y z : ℝ) : (x - z) ^ 2 ≤ 2 * ((x - y) ^ 2 + (y - z) ^ 2) := by sorry