Free triangles in finite planar meshes

This file formalizes Moise Chapter 3, Theorem 3 in the form needed by the polygonal Schoenflies induction. A finite planar triangle mesh with infinite frontier has an edge incident to exactly one triangle, hence a free triangle that can be removed by a supported ambient move.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCarrier (M : TriangleMesh) (t : Finset M.Vertex) : Set Plane

The geometric carrier of a maximal triangle.

Equations

• M.triangleCarrier t = (convexHull ℝ) (M.position '' ↑t)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edges (M : TriangleMesh) : Finset (Finset M.Vertex)

The two-element faces occurring in maximal triangles.

Equations

• M.edges = M.triangles.biUnion fun (t : Finset M.Vertex) => Finset.powersetCard 2 t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.incidentTriangles (M : TriangleMesh) (e : Finset M.Vertex) : Finset (Finset M.Vertex)

Maximal triangles incident to an edge.

Equations

• M.incidentTriangles e = {t ∈ M.triangles | e ⊆ t}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsBoundaryEdge (M : TriangleMesh) (e : Finset M.Vertex) : Prop

A boundary edge is incident to exactly one maximal triangle.

Equations

• M.IsBoundaryEdge e = (e ∈ M.edges ∧ (M.incidentTriangles e).card = 1)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsFreeTriangle (M : TriangleMesh) (t : Finset M.Vertex) : Prop

A weakly free triangle contains an incidence-one edge. This is the boundary-edge precursor used to find Moise's geometrically free triangles; by itself it does not exclude an additional isolated boundary vertex.

Equations

• M.IsFreeTriangle t = (t ∈ M.triangles ∧ ∃ (e : Finset M.Vertex), M.IsBoundaryEdge e ∧ e ⊆ t)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdges (M : TriangleMesh) (t : Finset M.Vertex) : Finset (Finset M.Vertex)

The three abstract edges of a maximal triangle.

Equations

• M.triangleEdges t = Finset.powersetCard 2 t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryEdges (M : TriangleMesh) (t : Finset M.Vertex) : Finset (Finset M.Vertex)

The boundary edges belonging to a maximal triangle.

Equations

• M.boundaryEdges t = Finset.filter M.IsBoundaryEdge (M.triangleEdges t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.allBoundaryEdges (M : TriangleMesh) : Finset (Finset M.Vertex)

All incidence-one edges of a finite triangle mesh.

Equations

• M.allBoundaryEdges = Finset.filter M.IsBoundaryEdge M.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_allBoundaryEdges_iff (M : TriangleMesh) {e : Finset M.Vertex} : e ∈ M.allBoundaryEdges ↔ M.IsBoundaryEdge e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryCarrier (M : TriangleMesh) : Set Plane

The finite union of the geometric carriers of all incidence-one mesh edges.

Equations

• M.boundaryCarrier = ⋃ e ∈ M.allBoundaryEdges, (convexHull ℝ) (M.position '' ↑e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isCompact_boundaryCarrier (M : TriangleMesh) : IsCompact M.boundaryCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_of_mem_edges (M : TriangleMesh) {e : Finset M.Vertex} (he : e ∈ M.edges) : e.card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_incidentTriangles_iff (M : TriangleMesh) {e t : Finset M.Vertex} : t ∈ M.incidentTriangles e ↔ t ∈ M.triangles ∧ e ⊆ t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_biUnion_subset (M : TriangleMesh) (F : Finset (Finset M.Vertex)) : frontier (⋃ t ∈ F, M.triangleCarrier t) ⊆ ⋃ t ∈ F, frontier (M.triangleCarrier t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleIndexEquiv (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : Fin 3 ≃ ↥t

Index the vertices of a maximal triangle by Fin 3.

Equations

• M.triangleIndexEquiv ht = Fintype.equivOfCardEq ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleAffineBasis (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : AffineBasis (Fin 3) ℝ Plane

The vertices of a maximal planar triangle form an affine basis of the plane.

Equations

• M.triangleAffineBasis ht = { toFun := fun (i : Fin 3) => M.position ↑((M.triangleIndexEquiv ht) i), ind' := ⋯, tot' := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.range_triangleAffineBasis (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : Set.range ⇑(M.triangleAffineBasis ht) = M.position '' ↑t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdgeOpposite (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) (i : Fin 3) : Finset M.Vertex

The edge opposite an indexed vertex of a maximal triangle.

Equations

• M.triangleEdgeOpposite ht i = t.erase ↑((M.triangleIndexEquiv ht) i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdgeOpposite_card (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) (i : Fin 3) : (M.triangleEdgeOpposite ht i).card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEdgeOpposite_subset (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) (i : Fin 3) : M.triangleEdgeOpposite ht i ⊆ t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.image_compl_eq_triangleEdgeOpposite (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) (i : Fin 3) : ⇑(M.triangleAffineBasis ht) '' {i}ᶜ = M.position '' ↑(M.triangleEdgeOpposite ht i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_edge_of_mem_frontier_triangle (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) {p : Plane} (hp : p ∈ frontier (M.triangleCarrier t)) : ∃ (e : Finset M.Vertex), e.card = 2 ∧ e ⊆ t ∧ p ∈ (convexHull ℝ) (M.position '' ↑e)

A nonvertex point on the frontier of a maximal triangle lies in one of its edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_eq_zero_of_mem_oppositeEdge (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) {p : Plane} (hp : p ∈ (convexHull ℝ) ↑(M.oppositeEdgePoints T k)) : (M.oppositeCoord T k) p = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_pos_of_mem_oppositeEdge_of_not_vertex (M : TriangleMesh) (T : M.Triangle) (k j : Fin 3) (hjk : j ≠ k) {p : Plane} (hp : p ∈ (convexHull ℝ) ↑(M.oppositeEdgePoints T k)) (hpv : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex T i)) : 0 < (M.oppositeCoord T j) p

At a nonvertex point of an edge, the two barycentric coordinates along the edge are positive.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_smul_eq_of_same_edge (M : TriangleMesh) (T U : M.Triangle) (kT kU : Fin 3) (hedge : M.oppositeEdgePoints T kT = M.oppositeEdgePoints U kU) : (M.oppositeCoord T kT) (M.position (M.orderedVertex U kU)) • M.oppositeCoord U kU = M.oppositeCoord T kT

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_ne_zero_of_same_edge (M : TriangleMesh) (T U : M.Triangle) (kT kU : Fin 3) (hedge : M.oppositeEdgePoints T kT = M.oppositeEdgePoints U kU) : (M.oppositeCoord T kT) (M.position (M.orderedVertex U kU)) ≠ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.interior_triangleCarrier (M : TriangleMesh) (T : M.Triangle) : interior (M.triangleCarrier ↑T) = {p : Plane | ∀ (i : Fin 3), 0 < (M.oppositeCoord T i) p}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.interior_triangleCarrier_nonempty (M : TriangleMesh) (T : M.Triangle) : (interior (M.triangleCarrier ↑T)).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.closure_interior_triangleCarrier (M : TriangleMesh) (T : M.Triangle) : closure (interior (M.triangleCarrier ↑T)) = M.triangleCarrier ↑T

A nondegenerate closed triangle is the closure of its Euclidean interior.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.disjoint_interior_triangleCarrier_convexHull_of_subset_card_le_two (M : TriangleMesh) (T : M.Triangle) {s : Finset M.Vertex} (hs : s ⊆ ↑T) (hcard : s.card ≤ 2) : Disjoint (interior (M.triangleCarrier ↑T)) ((convexHull ℝ) (M.position '' ↑s))

The interior of a maximal triangle misses the carrier of every proper face of that triangle. The formulation with an arbitrary set of at most two vertices is convenient when restricting a mesh along an existing edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.disjoint_interior_triangleCarrier_edgeCarrier (M : TriangleMesh) (T : M.Triangle) {e : Finset M.Vertex} (he : e ∈ M.edges) : Disjoint (interior (M.triangleCarrier ↑T)) ((convexHull ℝ) (M.position '' ↑e))

The interior of every maximal triangle misses every edge carrier of the mesh, whether or not that edge belongs to the triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.disjoint_interior_triangleCarrier_triangleCarrier (M : TriangleMesh) {T U : M.Triangle} (hne : ↑T ≠ ↑U) : Disjoint (interior (M.triangleCarrier ↑T)) (M.triangleCarrier ↑U)

The interior of one maximal triangle misses the full carrier of every distinct maximal triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.eq_of_interior_triangleCarrier_inter_nonempty (M : TriangleMesh) (T U : M.Triangle) (hinterior : (interior (M.triangleCarrier ↑T) ∩ interior (M.triangleCarrier ↑U)).Nonempty) : ↑T = ↑U

Maximal triangles in a face-to-face mesh have disjoint interiors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.disjoint_interior_triangleCarrier (M : TriangleMesh) {T U : M.Triangle} (hne : ↑T ≠ ↑U) : Disjoint (interior (M.triangleCarrier ↑T)) (interior (M.triangleCarrier ↑U))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.eraseTriangle_support_eq_closure_diff_triangleCarrier (M : TriangleMesh) (T : M.Triangle) : (M.eraseTriangle ↑T).toPlaneComplex.support = closure (M.toPlaneComplex.support \ M.triangleCarrier ↑T)

Deleting a maximal triangle leaves precisely the closure of the part of the old support outside that triangle. This is the face-to-face form of the elementary observation used in Moise's free-triangle removal: points on a surviving triangle are limits of points in its interior, and the interior of a different maximal triangle misses the deleted carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.disjoint_eraseTriangle_support_interior_triangleCarrier (M : TriangleMesh) (T : M.Triangle) : Disjoint (M.eraseTriangle ↑T).toPlaneComplex.support (interior (M.triangleCarrier ↑T))

The remaining support cannot contain an interior point of the deleted triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_eraseTriangle_support (M : TriangleMesh) (T : M.Triangle) : frontier (M.eraseTriangle ↑T).toPlaneComplex.support = frontier M.toPlaneComplex.support \ M.triangleCarrier ↑T ∪ (M.eraseTriangle ↑T).toPlaneComplex.support ∩ M.triangleCarrier ↑T

The frontier after deleting a maximal triangle consists of the old frontier away from the triangle together with the exact attachment of the surviving support to that triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCarrier_eq_nonnegCoords (M : TriangleMesh) (T : M.Triangle) : M.triangleCarrier ↑T = {p : Plane | ∀ (i : Fin 3), 0 ≤ (M.oppositeCoord T i) p}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.nonOppositeCoordNeighborhood (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : Set Plane

A neighborhood of a relative interior point of an edge, retaining positivity of all barycentric coordinates tangent to that edge.

Equations

• M.nonOppositeCoordNeighborhood T k = {p : LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane | ∀ (j : Fin 3), j ≠ k → 0 < (M.oppositeCoord T j) p}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.isOpen_nonOppositeCoordNeighborhood (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) : IsOpen (M.nonOppositeCoordNeighborhood T k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_nonOppositeCoordNeighborhood_of_mem_edge (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) {p : Plane} (hp : p ∈ (convexHull ℝ) ↑(M.oppositeEdgePoints T k)) (hpv : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex T i)) : p ∈ M.nonOppositeCoordNeighborhood T k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangle_inter_eq_edge (M : TriangleMesh) {T U : M.Triangle} (hTU : ↑T ≠ ↑U) {e : Finset M.Vertex} (hecard : e.card = 2) (heT : e ⊆ ↑T) (heU : e ⊆ ↑U) : ↑T ∩ ↑U = e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_negative_across_shared_edge (M : TriangleMesh) {T U : M.Triangle} (hTU : ↑T ≠ ↑U) {e : Finset M.Vertex} (hecard : e.card = 2) (heT : e ⊆ ↑T) (heU : e ⊆ ↑U) (kT kU : Fin 3) (hedgeT : M.oppositeEdgePoints T kT = Finset.image M.position e) (hedgeU : M.oppositeEdgePoints U kU = Finset.image M.position e) {p : Plane} (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpvT : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex T i)) (hpvU : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex U i)) : (M.oppositeCoord T kT) (M.position (M.orderedVertex U kU)) < 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeCarrier_infinite (M : TriangleMesh) {e : Finset M.Vertex} (hecard : e.card = 2) : ((convexHull ℝ) (M.position '' ↑e)).Infinite

A genuine geometric edge contains infinitely many points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_nonvertex_mem_edgeCarrier (M : TriangleMesh) {e : Finset M.Vertex} (hecard : e.card = 2) : ∃ p ∈ (convexHull ℝ) (M.position '' ↑e), ∀ (v : M.Vertex), p ≠ M.position v

Choose a relative-interior edge point which is not any vertex of the finite mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edge_eq_of_nonvertex_mem_edgeCarriers (M : TriangleMesh) {e f : Finset M.Vertex} (he : e ∈ M.edges) (hf : f ∈ M.edges) {p : Plane} (hpe : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpf : p ∈ (convexHull ℝ) (M.position '' ↑f)) (hpv : ∀ (v : M.Vertex), p ≠ M.position v) : e = f

Two mesh edges containing the same nonvertex point are the same edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeCarrier_inter_edgeCarrier (M : TriangleMesh) {e f : Finset M.Vertex} (he : e ∈ M.edges) (hf : f ∈ M.edges) : (convexHull ℝ) (M.position '' ↑e) ∩ (convexHull ℝ) (M.position '' ↑f) = (convexHull ℝ) (M.position '' ↑(e ∩ f))

Edge carriers in a face-to-face mesh meet in exactly the carrier of their common vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.vertex_mem_edge_of_position_mem_edgeCarrier (M : TriangleMesh) {v : M.Vertex} {e t : Finset M.Vertex} (ht : t ∈ M.triangles) (hvt : v ∈ t) (he : e ∈ M.edges) (hv : M.position v ∈ (convexHull ℝ) (M.position '' ↑e)) : v ∈ e

A used mesh vertex lying on an edge carrier is one of that edge's abstract endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.incidentTriangle_eq_of_ne (M : TriangleMesh) {e t u v : Finset M.Vertex} (hecard : e.card = 2) (ht : t ∈ M.incidentTriangles e) (hu : u ∈ M.incidentTriangles e) (hv : v ∈ M.incidentTriangles e) (hut : u ≠ t) (hvt : v ≠ t) : u = v

In a face-to-face planar mesh, once one incident triangle is fixed there is at most one other triangle incident to the same edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_incidentTriangles_le_two (M : TriangleMesh) {e : Finset M.Vertex} (hecard : e.card = 2) : (M.incidentTriangles e).card ≤ 2

Every geometric edge of a face-to-face planar mesh is incident to at most two triangles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edge_subset_of_nonvertex_mem_triangleCarrier (M : TriangleMesh) {e t u : Finset M.Vertex} {p : Plane} (hecard : e.card = 2) (het : e ⊆ t) (ht : t ∈ M.triangles) (hu : u ∈ M.triangles) (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpU : p ∈ M.triangleCarrier u) (hpv : ∀ (v : M.Vertex), p ≠ M.position v) : e ⊆ u

If a nonvertex point of an edge of t also belongs to u, then u contains the whole edge. This is the face-to-face property upgraded from geometry to incidence.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_frontier_of_mem_boundaryEdge (M : TriangleMesh) {e : Finset M.Vertex} (he : M.IsBoundaryEdge e) {p : Plane} (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpv : ∀ (v : M.Vertex), p ≠ M.position v) : p ∈ frontier M.toPlaneComplex.support

Every nonvertex point of an incidence-one edge lies on the support frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryEdgeCarrier_subset_frontier (M : TriangleMesh) {e : Finset M.Vertex} (he : M.IsBoundaryEdge e) : (convexHull ℝ) (M.position '' ↑e) ⊆ frontier M.toPlaneComplex.support

The whole carrier of an incidence-one edge lies in the support frontier, including endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryCarrier_subset_frontier (M : TriangleMesh) : M.boundaryCarrier ⊆ frontier M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_triangleEdges (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : (M.triangleEdges t).card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryEdges_subset_triangleEdges (M : TriangleMesh) (t : Finset M.Vertex) : M.boundaryEdges t ⊆ M.triangleEdges t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_boundaryEdges_iff (M : TriangleMesh) {e t : Finset M.Vertex} : e ∈ M.boundaryEdges t ↔ e ⊆ t ∧ e.card = 2 ∧ M.IsBoundaryEdge e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryEdges_nonempty_of_isFreeTriangle (M : TriangleMesh) {t : Finset M.Vertex} (ht : M.IsFreeTriangle t) : (M.boundaryEdges t).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_incidentTriangles_eq_two_of_not_boundary (M : TriangleMesh) {e t : Finset M.Vertex} (ht : t ∈ M.triangles) (hecard : e.card = 2) (het : e ⊆ t) (he : ¬M.IsBoundaryEdge e) : (M.incidentTriangles e).card = 2

A non-boundary edge of a maximal triangle has exactly two incident triangles.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.AreEdgeNeighbors (M : TriangleMesh) (t u : Finset M.Vertex) : Prop

Two maximal triangles are edge-neighbors if they contain a common two-vertex face.

Equations

• M.AreEdgeNeighbors t u = ∃ (e : Finset M.Vertex), e.card = 2 ∧ e ⊆ t ∧ e ⊆ u

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_boundaryEdges_le_two_of_neighbor (M : TriangleMesh) {t u : Finset M.Vertex} (ht : t ∈ M.triangles) (hu : u ∈ M.triangles) (htu : t ≠ u) (hneigh : M.AreEdgeNeighbors t u) : (M.boundaryEdges t).card ≤ 2

A triangle with an edge-neighbor cannot have all three edges on the boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_interior_union_triangleCarrier_of_shared_edge (M : TriangleMesh) {T U : M.Triangle} (hTU : ↑T ≠ ↑U) {e : Finset M.Vertex} (hecard : e.card = 2) (heT : e ⊆ ↑T) (heU : e ⊆ ↑U) {p : Plane} (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpvT : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex T i)) (hpvU : ∀ (i : Fin 3), p ≠ M.position (M.orderedVertex U i)) : p ∈ interior (M.triangleCarrier ↑T ∪ M.triangleCarrier ↑U)

Two distinct face-to-face triangles fill a neighborhood of every nonvertex point of their common edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_ne_of_not_mem_edgeVertices (M : TriangleMesh) (T : M.Triangle) (k : Fin 3) {e : Finset M.Vertex} (hedge : M.oppositeEdgePoints T k = Finset.image M.position e) {p : Plane} (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpNotVertices : p ∉ M.position '' ↑e) (i : Fin 3) : p ≠ M.position (M.orderedVertex T i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_interior_union_triangleCarrier_of_shared_edge_of_not_mem_edgeVertices (M : TriangleMesh) {T U : M.Triangle} (hTU : ↑T ≠ ↑U) {e : Finset M.Vertex} (hecard : e.card = 2) (heT : e ⊆ ↑T) (heU : e ⊆ ↑U) {p : Plane} (hpEdge : p ∈ (convexHull ℝ) (M.position '' ↑e)) (hpNotVertices : p ∉ M.position '' ↑e) : p ∈ interior (M.triangleCarrier ↑T ∪ M.triangleCarrier ↑U)

The shared-edge neighborhood theorem only needs the point to avoid the two endpoints of the common edge; unrelated retained mesh vertices are irrelevant.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeCarrier_diff_vertices_subset_interior_support (M : TriangleMesh) {e t : Finset M.Vertex} (ht : t ∈ M.triangles) (hecard : e.card = 2) (heT : e ⊆ t) (heNotBoundary : ¬M.IsBoundaryEdge e) : (convexHull ℝ) (M.position '' ↑e) \ M.position '' ↑e ⊆ interior M.toPlaneComplex.support

Every non-endpoint point of a non-boundary mesh edge is interior to the mesh support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_boundaryEdge_through_frontier_point (M : TriangleMesh) {p : Plane} (hpFrontier : p ∈ frontier M.toPlaneComplex.support) (hpv : ∀ (v : M.Vertex), p ≠ M.position v) : ∃ t ∈ M.triangles, ∃ (e : Finset M.Vertex), M.IsBoundaryEdge e ∧ e ⊆ t ∧ p ∈ (convexHull ℝ) (M.position '' ↑e)

Every nonvertex point of the support frontier lies on an incidence-one mesh edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_frontier_iff_exists_boundaryEdge_of_nonvertex (M : TriangleMesh) {p : Plane} (hpv : ∀ (v : M.Vertex), p ≠ M.position v) : p ∈ frontier M.toPlaneComplex.support ↔ ∃ (e : Finset M.Vertex), M.IsBoundaryEdge e ∧ p ∈ (convexHull ℝ) (M.position '' ↑e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_inter_triangleCarrier_diff_vertices (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : (frontier M.toPlaneComplex.support ∩ M.triangleCarrier t) \ Set.range M.position = (⋃ e ∈ M.boundaryEdges t, (convexHull ℝ) (M.position '' ↑e)) \ Set.range M.position

Away from mesh vertices, a triangle's frontier trace is exactly the union of its incidence-one edges. Extra isolated frontier vertices are precisely the obstruction addressed by Moise's cutting induction.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.HasNoIsolatedFrontierVertex (M : TriangleMesh) (t : Finset M.Vertex) : Prop

No mesh vertex contributes an isolated point to this triangle's frontier trace.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.vertex_mem_triangle_of_frontier_not_mem_boundaryEdges (M : TriangleMesh) (T : M.Triangle) (v : M.Vertex) (hvFrontier : M.position v ∈ frontier M.toPlaneComplex.support) (hvTriangle : M.position v ∈ M.triangleCarrier ↑T) (hvBoundary : ∀ e ∈ M.boundaryEdges ↑T, M.position v ∉ (convexHull ℝ) (M.position '' ↑e)) : v ∈ ↑T

An isolated point in a triangle's frontier trace must be one of the triangle's own vertices. This remains valid when the mesh vertex type contains unused retained vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.hasNoIsolatedFrontierVertex_of_boundaryEdges_card_two (M : TriangleMesh) (T : M.Triangle) (hcard : (M.boundaryEdges ↑T).card = 2) : M.HasNoIsolatedFrontierVertex ↑T

If two edges of a maximal triangle are boundary edges, every frontier vertex on that triangle lies on one of them.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_inter_triangleCarrier_eq_boundaryEdges (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) (hvertices : M.HasNoIsolatedFrontierVertex t) : frontier M.toPlaneComplex.support ∩ M.triangleCarrier t = ⋃ e ∈ M.boundaryEdges t, (convexHull ℝ) (M.position '' ↑e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_free_triangle (M : TriangleMesh) (hfrontier : (frontier M.toPlaneComplex.support).Infinite) : ∃ (t : Finset M.Vertex), M.IsFreeTriangle t

An infinite frontier of a finite face-to-face planar mesh contains a boundary edge. This is the weak free-triangle existence theorem used at the start of Moise's finite induction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.frontier_infinite_of_triangles_nonempty (M : TriangleMesh) (hne : M.triangles.Nonempty) : (frontier M.toPlaneComplex.support).Infinite

The frontier of every nonempty finite planar triangle mesh is infinite.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_free_triangle_of_triangles_nonempty (M : TriangleMesh) (hne : M.triangles.Nonempty) : ∃ (t : Finset M.Vertex), M.IsFreeTriangle t