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

def Polygon.HasNondegenerateEdges {P : Type u_3} {n : ℕ} (poly : Polygon P n) : Prop

A polygon has nondegenerate edges if adjacent vertices are distinct.

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.

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.

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.

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.

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.

@[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.

@[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.