Polygons

This file defines polygons in affine spaces.

Main definitions

• Polygon P n: A polygon with n vertices in a type P.

structure Polygon (P : Type u_1) (n : ℕ) : Type u_1

A polygon with n vertices in a type P.

• vertices : Fin n → P

  The vertices of the polygon, indexed by Fin n.

instance Polygon.instCoeFunForallFin {P : Type u_3} {n : ℕ} : CoeFun (Polygon P n) fun (x : Polygon P n) => Fin n → P

A coercion to function so that vertices can be written as poly i instead of poly.vertices i

Equations

• Polygon.instCoeFunForallFin = { coe := Polygon.vertices }

def Polygon.edgePath (R : Type u_1) {V : Type u_2} {P : Type u_3} {n : ℕ} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NeZero n] (poly : Polygon P n) (i : Fin n) : R →ᵃ[R] P

The i-th edge as an affine map R →ᵃ[R] P.

Equations

• Polygon.edgePath R poly i = AffineMap.lineMap (poly.vertices i) (poly.vertices (i + 1))

def Polygon.edgeSet (R : Type u_1) {V : Type u_2} {P : Type u_3} {n : ℕ} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NeZero n] [PartialOrder R] (poly : Polygon P n) (i : Fin n) : Set P

The i-th edge as a set of points using an affineSegment.

Equations

• Polygon.edgeSet R poly i = affineSegment R (poly.vertices i) (poly.vertices (i + 1))

theorem Polygon.edgeSet_eq_image_edgePath (R : Type u_1) {V : Type u_2} {P : Type u_3} {n : ℕ} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NeZero n] [PartialOrder R] (poly : Polygon P n) (i : Fin n) : edgeSet R poly i = ⇑(edgePath R poly i) '' Set.Icc 0 1

The edgeSet is equivalent to the image of the edgePath.

def Polygon.boundary (R : Type u_1) {V : Type u_2} {P : Type u_3} {n : ℕ} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] [NeZero n] [PartialOrder R] (poly : Polygon P n) : Set P

The boundary of the polygon is the union of all its edges.

Equations

• Polygon.boundary R poly = ⋃ (i : Fin n), Polygon.edgeSet R poly i