Signed area as the standard orientation form

Proved

Batch3N9.Problem97.signedArea2_eq_stdOrientation_areaForm

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

The signed area of three planar points equals the standard orientation area form applied to the two displacement vectors.

Preamble

import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation
import Definitions.Def_Erdos9796Counting_SignedAreaOangle
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
open Problem97
open scoped EuclideanGeometry

Formal statement

theorem Batch3N9.Problem97.signedArea2_eq_stdOrientation_areaForm (v vj vk : ℝ²) : Problem97.signedArea2 v vj vk = stdOrientation.areaForm (vj - v) (vk - v) := by sorry

Source

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

View graph