Polygons

This file defines polygons in affine spaces. For the special case n = 3, an interconversion is provided with Affine.Triangle.

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.

@[implicit_reducible]

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.HasNondegenerateEdges {P : Type u_3} {n : ℕ} (poly : Polygon P n) : Prop

A polygon has nondegenerate edges if adjacent vertices are distinct.

Equations

• poly.HasNondegenerateEdges = ∀ (i : Fin n), poly.vertices i ≠ poly.vertices ((finRotate n) i)

theorem Polygon.HasNondegenerateEdges.two_le {P : Type u_3} {n : ℕ} [NeZero n] {poly : Polygon P n} (h : poly.HasNondegenerateEdges) : 2 ≤ n

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] (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 ((finRotate n) i))

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] [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 ((finRotate n) i))

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] [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] [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

def Polygon.HasNondegenerateVertices (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) : Prop

A polygon has nondegenerate vertices if any three consecutive vertices are affinely independent.

Equations

• Polygon.HasNondegenerateVertices R poly = ∀ (i : Fin n), AffineIndependent R ![poly.vertices i, poly.vertices (i + 1), poly.vertices (i + 2)]

theorem Polygon.HasNondegenerateVertices.hasNondegenerateEdges {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] [Nontrivial R] {poly : Polygon P n} (h : HasNondegenerateVertices R poly) : poly.HasNondegenerateEdges

Polygons with nondegenerate vertices also have nondegenerate edges.

theorem Polygon.HasNondegenerateVertices.three_le {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] [Nontrivial R] {poly : Polygon P n} (h : HasNondegenerateVertices R poly) : 3 ≤ n

Interconversion with Affine.Triangle

def Affine.Triangle.toPolygon {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] : Triangle R P ↪ Polygon P 3

Embedding from affine triangles to polygons with 3 vertices.

Equations

• Affine.Triangle.toPolygon = { toFun := fun (t : Affine.Triangle R P) => { vertices := t.points }, inj' := ⋯ }

@[simp]

theorem Affine.Triangle.toPolygon_vertices {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (t : Triangle R P) : (toPolygon t).vertices = t.points

def Polygon.toTriangle (R : Type u_1) {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : Polygon P 3) (h : HasNondegenerateVertices R p) : Affine.Triangle R P

Convert a polygon with 3 nondegenerate vertices to an Affine.Triangle.

Equations

• Polygon.toTriangle R p h = { points := p.vertices, independent := ⋯ }

@[simp]

theorem Polygon.toTriangle_points {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : Polygon P 3) (h : HasNondegenerateVertices R p) : (toTriangle R p h).points = p.vertices

@[simp]

theorem Polygon.toTriangle_toPolygon {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (poly : Polygon P 3) (h : HasNondegenerateVertices R poly) : Affine.Triangle.toPolygon (toTriangle R poly h) = poly

Converting a 3-polygon to a triangle and back yields the original polygon.

theorem Affine.Triangle.toPolygon_hasNondegenerateVertices {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (t : Triangle R P) : Polygon.HasNondegenerateVertices R (toPolygon t)

The polygon obtained from a triangle has nondegenerate vertices.

@[simp]

theorem Affine.Triangle.toPolygon_toTriangle {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V P] (t : Triangle R P) : Polygon.toTriangle R (toPolygon t) ⋯ = t

Converting a triangle to a polygon and back yields the original triangle.