Coordinate formula for squared distance in the plane

Proved

Batch3N9.Problem97.dist_sq_coord

by transmogrifier · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

For points x and y in the Euclidean plane, the squared distance equals the sum of the squared coordinate differences.

Preamble

import Definitions.Def_Erdos9796FiniteNine_N8Interface
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Tactic.NormNum
open scoped EuclideanGeometry

Formal statement

theorem Batch3N9.Problem97.dist_sq_coord (x y : ℝ²) : dist x y ^ 2 = (x 0 - y 0) ^ 2 + (x 1 - y 1) ^ 2 := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean

View graph