Finite unions of polygonal disks

The cellwise intrinsic approximation produces finitely many polygonal closed disks whose interiors are compatible. Independently chosen disk triangulations need not agree on their common boundary segments. This file instead cuts one enclosing triangle by every edge line in the family and retains precisely the chambers lying inside at least one polygon. The resulting single triangle mesh has support equal to the union.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coordinateEmbed (M : TriangleMesh) : ↑(GeometricRealization M.Vertex M.triangles) → Plane

The canonical barycentric embedding of a finite plane triangle mesh realization.

Equations

• M.coordinateEmbed x = M.toPlaneComplex.baryEval ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isEmbedding_coordinateEmbed (M : TriangleMesh) : Topology.IsEmbedding M.coordinateEmbed

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.range_coordinateEmbed (M : TriangleMesh) : Set.range M.coordinateEmbed = M.toPlaneComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coordinateEmbedInto (M : TriangleMesh) (W : Set Plane) (hW : M.toPlaneComplex.support ⊆ W) : ↑(GeometricRealization M.Vertex M.triangles) → ↑W

Restrict the coordinate embedding to any plane region containing the mesh support.

Equations

• M.coordinateEmbedInto W hW x = ⟨M.coordinateEmbed x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isEmbedding_coordinateEmbedInto (M : TriangleMesh) (W : Set Plane) (hW : M.toPlaneComplex.support ⊆ W) : Topology.IsEmbedding (M.coordinateEmbedInto W hW)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion {ι : Type u_1} (J : ι → PolygonalCircle) : Set Plane

The union of the finitely many closed polygonal disks.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion J = ⋃ (i : ι), (J i).closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.isCompact_closedRegion {ι : Type u_1} (J : ι → PolygonalCircle) [Finite ι] : IsCompact (closedRegion J)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.enclosingRadius {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : ℝ

A positive radius of a ball containing every disk in the family.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.enclosingRadius J = max ⋯.choose 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.enclosingRadius_pos {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : 0 < enclosingRadius J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion_subset_enclosingBall {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : closedRegion J ⊆ Metric.closedBall 0 (enclosingRadius J)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.enclosingMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : TriangleMesh

The common enclosing triangle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion_subset_enclosingMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : closedRegion J ⊆ (enclosingMesh J).toPlaneComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.edgeLines {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : List (Plane →ᵃ[ℝ] ℝ)

Every supporting line of every polygon in the family.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.edgeLines J = List.flatMap (fun (i : ι) => (J i).edgeLines) Finset.univ.toList

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.edgeLine_mem_edgeLines {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (i : ι) (k : ZMod (J i).n) : (J i).edgeLine k ∈ edgeLines J

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : TriangleMesh

The common supporting-line arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : (arrangementMesh J).toPlaneComplex.support = (enclosingMesh J).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion_subset_arrangementMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : closedRegion J ⊆ (arrangementMesh J).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementMesh_isMonochromatic {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (i : ι) (k : ZMod (J i).n) : (arrangementMesh J).IsMonochromatic ((J i).edgeLine k)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangleCarrier {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (t : Finset (arrangementMesh J).Vertex) : Set Plane

Carrier of one maximal chamber of the common arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.convex_arrangementTriangleCarrier {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (t : Finset (arrangementMesh J).Vertex) : Convex ℝ (arrangementTriangleCarrier J t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.isClosed_arrangementTriangleCarrier {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (t : Finset (arrangementMesh J).Vertex) : IsClosed (arrangementTriangleCarrier J t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangleCarrier_interior_nonempty {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) : (interior (arrangementTriangleCarrier J t)).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closure_interior_arrangementTriangleCarrier {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) : closure (interior (arrangementTriangleCarrier J t)) = arrangementTriangleCarrier J t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangle_interior_disjoint_carrier {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (i : ι) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) : Disjoint (interior (arrangementTriangleCarrier J t)) (J i).carrier

Every open arrangement chamber misses every polygon boundary in the family.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangle_interior_side {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (i : ι) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) : interior (arrangementTriangleCarrier J t) ⊆ (J i).interiorRegion ∨ interior (arrangementTriangleCarrier J t) ⊆ (J i).exteriorRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsInteriorArrangementTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (t : Finset (arrangementMesh J).Vertex) : Prop

A chamber is retained when it lies on the bounded side of at least one polygon.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegionMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : TriangleMesh

The common finite mesh of the union of all closed regions.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegionMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {t : Finset (closedRegionMesh J).Vertex} : t ∈ (closedRegionMesh J).triangles ↔ t ∈ (arrangementMesh J).triangles ∧ IsInteriorArrangementTriangle J t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangleCarrier_subset_closedRegion {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) (hinside : IsInteriorArrangementTriangle J t) : arrangementTriangleCarrier J t ⊆ closedRegion J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegionMesh_support_subset {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : (closedRegionMesh J).toPlaneComplex.support ⊆ closedRegion J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.interiorRegion_subset_closedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (i : ι) : (J i).interiorRegion ⊆ (closedRegionMesh J).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion_subset_closedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : closedRegion J ⊆ (closedRegionMesh J).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) : (closedRegionMesh J).toPlaneComplex.support = closedRegion J

Exact support of the common family mesh.

Synchronized submeshes of one family arrangement

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegion {ι : Type u_1} (J : ι → PolygonalCircle) (p : ι → Prop) : Set Plane

The union of a selected subfamily of polygonal closed disks.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegion J p = ⋃ (i : ι), ⋃ (_ : p i), (J i).closedRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsSelectedInteriorArrangementTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) (t : Finset (arrangementMesh J).Vertex) : Prop

An arrangement chamber belongs to the selected submesh when its interior lies on the bounded side of one selected polygon.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) : TriangleMesh

Restrict the common arrangement to the chambers belonging to a selected subfamily. Different predicates therefore produce meshes with definitionally the same ambient vertex type and position map.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) {t : Finset (selectedClosedRegionMesh J p).Vertex} : t ∈ (selectedClosedRegionMesh J p).triangles ↔ t ∈ (arrangementMesh J).triangles ∧ IsSelectedInteriorArrangementTriangle J p t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementTriangleCarrier_subset_selectedClosedRegion {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) {t : Finset (arrangementMesh J).Vertex} (ht : t ∈ (arrangementMesh J).triangles) (hinside : IsSelectedInteriorArrangementTriangle J p t) : arrangementTriangleCarrier J t ⊆ selectedClosedRegion J p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMesh_support_subset {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) : (selectedClosedRegionMesh J p).toPlaneComplex.support ⊆ selectedClosedRegion J p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.interiorRegion_subset_selectedClosedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) (i : ι) (hpi : p i) : (J i).interiorRegion ⊆ (selectedClosedRegionMesh J p).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegion_subset_selectedClosedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) : selectedClosedRegion J p ⊆ (selectedClosedRegionMesh J p).toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p : ι → Prop) : (selectedClosedRegionMesh J p).toPlaneComplex.support = selectedClosedRegion J p

Every selected subfamily is recovered exactly as a face restriction of the one common arrangement. This is the conforming old/new submesh interface used by the Radó weld.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMesh_triangles_union {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p q : ι → Prop) : (selectedClosedRegionMesh J p).triangles ∪ (selectedClosedRegionMesh J q).triangles = (selectedClosedRegionMesh J fun (i : ι) => p i ∨ q i).triangles

Taking the union of two selected submeshes is literally the selection by the disjunction of the two predicates. All three meshes use the same ambient arrangement vertex type.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedClosedRegionMeshes_joint_edge_valence {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (p q : ι → Prop) (e : Finset (arrangementMesh J).Vertex) (he : e.card = 2) : {t ∈ (selectedClosedRegionMesh J p).triangles ∪ (selectedClosedRegionMesh J q).triangles | e ⊆ t}.card ≤ 2

The two synchronized selected submeshes jointly retain the planar surface incidence bound: every two-vertex edge belongs to at most two triangles. This is inherited from the single ambient arrangement, not proved separately for the two selections.

Synchronization with an independent finite patch mesh

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.synchronizedArrangement {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) : TriangleMesh

Cut the polygon-family arrangement by all barycentric face lines of a second mesh.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.synchronizedArrangement J N = (LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.arrangementMesh J).refineTo N

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsSelectedSynchronizedTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (p : ι → Prop) (t : Finset (synchronizedArrangement J N).Vertex) : Prop

A chamber of the synchronized arrangement lies in the selected polygonal region.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedSynchronizedMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (p : ι → Prop) : TriangleMesh

The polygonal side of the common old/patch arrangement.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsTargetSynchronizedTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (t : Finset (synchronizedArrangement J N).Vertex) : Prop

The patch side consists of the synchronized chambers whose interiors meet the patch.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetSynchronizedMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) : TriangleMesh

The target-mesh side of the common old/patch arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedSynchronizedMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (p : ι → Prop) {t : Finset (selectedSynchronizedMesh J N p).Vertex} : t ∈ (selectedSynchronizedMesh J N p).triangles ↔ t ∈ (synchronizedArrangement J N).triangles ∧ IsSelectedSynchronizedTriangle J N p t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetSynchronizedMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) {t : Finset (targetSynchronizedMesh J N).Vertex} : t ∈ (targetSynchronizedMesh J N).triangles ↔ t ∈ (synchronizedArrangement J N).triangles ∧ IsTargetSynchronizedTriangle J N t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.exists_arrangementTriangle_of_synchronized {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {N : TriangleMesh} {t : Finset (synchronizedArrangement J N).Vertex} (ht : t ∈ (synchronizedArrangement J N).triangles) : ∃ u ∈ (arrangementMesh J).triangles, (synchronizedArrangement J N).triangleCarrier t ⊆ (arrangementMesh J).triangleCarrier u

Every synchronized chamber is contained in one chamber of the original polygon-family arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.synchronizedTriangle_interior_side {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (i : ι) {t : Finset (synchronizedArrangement J N).Vertex} (ht : t ∈ (synchronizedArrangement J N).triangles) : interior ((synchronizedArrangement J N).triangleCarrier t) ⊆ (J i).interiorRegion ∨ interior ((synchronizedArrangement J N).triangleCarrier t) ⊆ (J i).exteriorRegion

Synchronized chambers still lie wholly on one side of every family polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedSynchronizedMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (p : ι → Prop) : (selectedSynchronizedMesh J N p).toPlaneComplex.support = selectedClosedRegion J p

Further cutting by the target mesh does not change the selected polygonal support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetSynchronizedMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (hsub : N.toPlaneComplex.support ⊆ (arrangementMesh J).toPlaneComplex.support) : (targetSynchronizedMesh J N).toPlaneComplex.support = N.toPlaneComplex.support

When the target support lies in the family arrangement's enclosing triangle, the target side of the synchronized arrangement recovers it exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.synchronizedMeshes_joint_edge_valence {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (p : ι → Prop) (e : Finset (synchronizedArrangement J N).Vertex) (he : e.card = 2) : {t ∈ (selectedSynchronizedMesh J N p).triangles ∪ (targetSynchronizedMesh J N).triangles | e ⊆ t}.card ≤ 2

The synchronized old and target submeshes jointly satisfy the planar edge-incidence bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.closedRegion_is_polyhedron {ι : Type u_1} (J : ι → PolygonalCircle) [Finite ι] : ∃ (K : PlaneComplex), K.support = closedRegion J ∧ K.IsPure2

A finite union of polygonal closed disks is a finite pure plane polyhedron.