lean_workbook_plus_78256
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78256 : ∀ x y z : ℝ, (z - x) ^ 2 / 2 ≤ (y - x) ^ 2 + (z - y) ^ 2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78256 : ∀ x y z : ℝ, (z - x) ^ 2 / 2 ≤ (y - x) ^ 2 + (z - y) ^ 2 := by sorry