Prove2Me

lean_workbook_plus_13428

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if aa , bb , cc , dd , ee , and ff are real numbers, \n

(a−c)2+(b−d)2+(c−e)2+(d−f)2≥(e−a)2+(f−b)2.\sqrt{(a-c)^2+(b-d)^2}+\sqrt{(c-e)^2+(d-f)^2}\geq\sqrt{(e-a)^2+(f-b)^2}.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13428 (a b c d e f : ℝ) : Real.sqrt ((a - c) ^ 2 + (b - d) ^ 2) + Real.sqrt ((a - e) ^ 2 + (b - f) ^ 2) ≥ Real.sqrt ((e - a) ^ 2 + (f - b) ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph