Polygonal Jordan regions as finite plane complexes

This file formalizes Moise Chapter 2, Theorem 2. The finitely many affine lines containing the edges of a polygon cut an enclosing triangle into a finite triangle mesh. The triangles on the bounded side of polygonal Jordan form the required finite complex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeNormalLinear (p q : Plane) : Plane →ₗ[ℝ] ℝ

The linear functional whose zero set is parallel to the vector from p to q.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine (J : PolygonalCircle) (i : ZMod J.n) : Plane →ᵃ[ℝ] ℝ

An affine equation for the line containing polygon edge i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine_initial (J : PolygonalCircle) (i : ZMod J.n) : (J.edgeLine i) (J.vertex i) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine_terminal (J : PolygonalCircle) (i : ZMod J.n) : (J.edgeLine i) (J.vertex (i + 1)) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine_eq_zero_of_mem_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) {x : Plane} (hx : x ∈ J.edgeSegment i) : (J.edgeLine i) x = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine_surjective (J : PolygonalCircle) (i : ZMod J.n) : Function.Surjective ⇑(J.edgeLine i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_edgeLine_nonneg (J : PolygonalCircle) (i : ZMod J.n) : interior {x : Plane | 0 ≤ (J.edgeLine i) x} = {x : Plane | 0 < (J.edgeLine i) x}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_edgeLine_nonpos (J : PolygonalCircle) (i : ZMod J.n) : interior {x : Plane | (J.edgeLine i) x ≤ 0} = {x : Plane | (J.edgeLine i) x < 0}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLines (J : PolygonalCircle) : List (Plane →ᵃ[ℝ] ℝ)

The finite list of supporting lines used in Moise's arrangement proof.

Equations

• J.edgeLines = List.map J.edgeLine Finset.univ.toList

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLine_mem_edgeLines (J : PolygonalCircle) (i : ZMod J.n) : J.edgeLine i ∈ J.edgeLines

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.enclosingRadius (J : PolygonalCircle) : ℝ

A positive radius of a closed ball containing the closed polygonal region.

Equations

• J.enclosingRadius = max ⋯.choose 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.enclosingRadius_pos (J : PolygonalCircle) : 0 < J.enclosingRadius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion_subset_enclosingBall (J : PolygonalCircle) : J.closedRegion ⊆ Metric.closedBall 0 J.enclosingRadius

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.enclosingTriangleVertices (R : ℝ) : Fin 3 → Plane

Vertices of a large triangle containing the ball of radius R.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.enclosingTriangleVertices_affineIndependent {R : ℝ} (hR : 0 < R) : AffineIndependent ℝ (enclosingTriangleVertices R)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedBall_subset_enclosingTriangle {R : ℝ} (hR : 0 < R) : Metric.closedBall 0 R ⊆ (convexHull ℝ) (Set.range (enclosingTriangleVertices R))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.enclosingMesh (J : PolygonalCircle) : TriangleMesh

The one-triangle seed mesh in which the supporting-line arrangement is constructed.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion_subset_enclosingMesh_support (J : PolygonalCircle) : J.closedRegion ⊆ J.enclosingMesh.toPlaneComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementMesh (J : PolygonalCircle) : TriangleMesh

The finite mesh obtained by cutting the enclosing triangle along every polygon edge line.

Equations

• J.arrangementMesh = J.enclosingMesh.refineByLines J.edgeLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementMesh_support (J : PolygonalCircle) : J.arrangementMesh.toPlaneComplex.support = J.enclosingMesh.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementMesh_isMonochromatic (J : PolygonalCircle) (i : ZMod J.n) : J.arrangementMesh.IsMonochromatic (J.edgeLine i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion_subset_arrangementMesh_support (J : PolygonalCircle) : J.closedRegion ⊆ J.arrangementMesh.toPlaneComplex.support

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementTriangleCarrier (J : PolygonalCircle) (t : Finset J.arrangementMesh.Vertex) : Set Plane

Carrier of one maximal triangle in the supporting-line arrangement.

Equations

• J.arrangementTriangleCarrier t = (convexHull ℝ) (J.arrangementMesh.position '' ↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.convex_arrangementTriangleCarrier (J : PolygonalCircle) (t : Finset J.arrangementMesh.Vertex) : Convex ℝ (J.arrangementTriangleCarrier t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isClosed_arrangementTriangleCarrier (J : PolygonalCircle) (t : Finset J.arrangementMesh.Vertex) : IsClosed (J.arrangementTriangleCarrier t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementTriangleCarrier_interior_nonempty (J : PolygonalCircle) {t : Finset J.arrangementMesh.Vertex} (ht : t ∈ J.arrangementMesh.triangles) : (interior (J.arrangementTriangleCarrier t)).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closure_interior_arrangementTriangleCarrier (J : PolygonalCircle) {t : Finset J.arrangementMesh.Vertex} (ht : t ∈ J.arrangementMesh.triangles) : closure (interior (J.arrangementTriangleCarrier t)) = J.arrangementTriangleCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementTriangle_interior_disjoint_carrier (J : PolygonalCircle) {t : Finset J.arrangementMesh.Vertex} (ht : t ∈ J.arrangementMesh.triangles) : Disjoint (interior (J.arrangementTriangleCarrier t)) J.carrier

Every open triangle chamber of the supporting-line arrangement misses the polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementTriangle_interior_side (J : PolygonalCircle) {t : Finset J.arrangementMesh.Vertex} (ht : t ∈ J.arrangementMesh.triangles) : interior (J.arrangementTriangleCarrier t) ⊆ J.interiorRegion ∨ interior (J.arrangementTriangleCarrier t) ⊆ J.exteriorRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.IsInteriorArrangementTriangle (J : PolygonalCircle) (t : Finset J.arrangementMesh.Vertex) : Prop

The arrangement chambers lying on the bounded side of the polygon.

Equations

• J.IsInteriorArrangementTriangle t = (interior (J.arrangementTriangleCarrier t) ⊆ J.interiorRegion)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegionMesh (J : PolygonalCircle) : TriangleMesh

The finite mesh formed by all bounded-side arrangement chambers.

Equations

• J.closedRegionMesh = J.arrangementMesh.restrictTriangles J.IsInteriorArrangementTriangle

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegionMesh_triangle_mem (J : PolygonalCircle) {t : Finset J.closedRegionMesh.Vertex} : t ∈ J.closedRegionMesh.triangles ↔ t ∈ J.arrangementMesh.triangles ∧ J.IsInteriorArrangementTriangle t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.arrangementTriangleCarrier_subset_closedRegion (J : PolygonalCircle) {t : Finset J.arrangementMesh.Vertex} (ht : t ∈ J.arrangementMesh.triangles) (hinside : J.IsInteriorArrangementTriangle t) : J.arrangementTriangleCarrier t ⊆ J.closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegionMesh_support_subset (J : PolygonalCircle) : J.closedRegionMesh.toPlaneComplex.support ⊆ J.closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interiorRegion_subset_closedRegionMesh_support (J : PolygonalCircle) : J.interiorRegion ⊆ J.closedRegionMesh.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegionMesh_support (J : PolygonalCircle) : J.closedRegionMesh.toPlaneComplex.support = J.closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_carrier_exteriorRegion (J : PolygonalCircle) : Disjoint J.carrier J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_closedRegion_exteriorRegion (J : PolygonalCircle) : Disjoint J.closedRegion J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_closedRegion (J : PolygonalCircle) : frontier J.closedRegion = J.carrier

The topological boundary of the closed polygonal disk is the original polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_closedRegion (J : PolygonalCircle) : interior J.closedRegion = J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isConnected_closedRegion (J : PolygonalCircle) : IsConnected J.closedRegion