Erdős 97 convex-octagon formalization: Basic

@[reducible, inline]

abbrev Erdos97Octagon.Plane : Type

The Euclidean plane, represented as EuclideanSpace ℝ (Fin 2).

Equations

• Erdos97Octagon.Plane = EuclideanSpace ℝ (Fin 2)