Finite surface triangulations

This finite incidence package is consumed by the cell-complex conversion and fed by the faithful GeometricTriangulation object through GeometricTriangulation.toFiniteSurfaceTriangulation. Radó's theorem enters as moise_triangulation, proved in ClassificationOfSurfaces/Moise/.

An arbitrary FiniteSurfaceTriangulation record does not certify that its incidence data describe its stored realization. The classification proof therefore starts from GeometricTriangulation and uses the incidence certificate constructed by its bridge.

inductive LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge (α : Type u_1) : Type u_1

An oriented use of an edge in a triangle boundary word.

• pos {α : Type u_1} : α → OrientedEdge α
• neg {α : Type u_1} : α → OrientedEdge α

def LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqOrientedEdge.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : OrientedEdge α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqOrientedEdge {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (OrientedEdge α✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqOrientedEdge = LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqOrientedEdge.decEq

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprOrientedEdge {α✝ : Type u_1} [Repr α✝] : Repr (OrientedEdge α✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprOrientedEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprOrientedEdge.repr }

def LeanEval.Topology.ClassificationOfSurfaces.instReprOrientedEdge.repr {α✝ : Type u_1} [Repr α✝] : OrientedEdge α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeOrientedEdge {α✝ : Type u_1} [Fintype α✝] : Fintype (OrientedEdge α✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instFintypeOrientedEdge = Fintype.ofEquiv (α✝ ⊕ α✝) (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.proxyTypeEquiv α✝)

def LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.edge {α : Type u_1} : OrientedEdge α → α

The underlying unoriented edge.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos a).edge = a
• (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg a).edge = a

def LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.flip {α : Type u_1} : OrientedEdge α → OrientedEdge α

Reverse an oriented edge.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos a).flip = LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg a
• (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg a).flip = LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.flip_flip {α : Type u_1} (e : OrientedEdge α) : e.flip.flip = e

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.Valid (Vertex : Type u_1) (Edge : Type u_2) (Triangle : Type u_3) [DecidableEq Vertex] (edgeVertices : Edge → Finset Vertex) (triangleVertices : Triangle → Finset Vertex) (edgeSource edgeTarget : Edge → Vertex) (triangleBoundary : Triangle → List (OrientedEdge Edge)) : Prop

Finite combinatorial validity data for the project triangulation object.

This deliberately stays close to what the current PL complex handoff can prove: edges have two vertices, triangles have three vertices, recorded endpoints lie on their edge, and every edge appearing in a triangle boundary is a face of that triangle. Cyclic ordering and quotient-realization geometry are separate theorem boundaries.

• edge_card (e : Edge) : (edgeVertices e).card = 2
• triangle_card (t : Triangle) : (triangleVertices t).card = 3
• edgeSource_mem (e : Edge) : edgeSource e ∈ edgeVertices e
• edgeTarget_mem (e : Edge) : edgeTarget e ∈ edgeVertices e
• edgeSource_ne_edgeTarget (e : Edge) : edgeSource e ≠ edgeTarget e
• boundary_edge_vertices_subset (t : Triangle) (oe : OrientedEdge Edge) : oe ∈ triangleBoundary t → edgeVertices oe.edge ⊆ triangleVertices t

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation (S : Type u_1) [TopologicalSpace S] : Type 1

A finite triangulation of a topological surface.

This should eventually be replaced by, or bridged to, the best available mathlib notion of finite simplicial/CW complex realization. For now it records the public API needed by the common triangulation-to-cell-complex bridge: finite incidence data, a topological realization, and a homeomorphism from that realization to the target surface.

• Vertex : Type

  The Vertex declaration.

• Edge : Type

  The Edge declaration.

• Triangle : Type

  The Triangle declaration.

• vertexFintype : Fintype self.Vertex
• vertexDecidableEq : DecidableEq self.Vertex
• edgeFintype : Fintype self.Edge
• triangleFintype : Fintype self.Triangle
• realization : Type

  The realization declaration.

• realizationTop : TopologicalSpace self.realization
• edgeVertices : self.Edge → Finset self.Vertex

  The edgeVertices declaration.

• triangleVertices : self.Triangle → Finset self.Vertex

  The triangleVertices declaration.

• edgeSource : self.Edge → self.Vertex

  The edgeSource declaration.

• edgeTarget : self.Edge → self.Vertex

  The edgeTarget declaration.

• triangleBoundary : self.Triangle → List (OrientedEdge self.Edge)

  The triangleBoundary declaration.

• edgeIsBoundary : self.Edge → Prop

  The edgeIsBoundary declaration.

• isSurfaceTriangulation : Valid self.Vertex self.Edge self.Triangle self.edgeVertices self.triangleVertices self.edgeSource self.edgeTarget self.triangleBoundary
• homeomorphSurface : Nonempty (self.realization ≃ₜ S)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.numVertices {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : ℕ

Number of vertices in a finite surface triangulation.

Equations

• T.numVertices = Fintype.card T.Vertex

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.numEdges {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : ℕ

Number of edges in a finite surface triangulation.

Equations

• T.numEdges = Fintype.card T.Edge

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.numTriangles {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : ℕ

Number of triangles in a finite surface triangulation.

Equations

• T.numTriangles = Fintype.card T.Triangle

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.orientedEdgeSource {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : OrientedEdge T.Edge → T.Vertex

Source vertex of an oriented edge occurrence in a triangulation.

Equations

• T.orientedEdgeSource (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos e) = T.edgeSource e
• T.orientedEdgeSource (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg e) = T.edgeTarget e

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.orientedEdgeTarget {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : OrientedEdge T.Edge → T.Vertex

Target vertex of an oriented edge occurrence in a triangulation.

Equations

• T.orientedEdgeTarget (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos e) = T.edgeTarget e
• T.orientedEdgeTarget (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg e) = T.edgeSource e

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.BoundaryPosition {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : Type

A position in one of the stored oriented triangle boundaries.

Equations

• T.BoundaryPosition = ((t : T.Triangle) × Fin (T.triangleBoundary t).length)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.BoundaryPosition.orientedEdge {S : Type u_1} [TopologicalSpace S] {T : FiniteSurfaceTriangulation S} (o : T.BoundaryPosition) : OrientedEdge T.Edge

The oriented edge stored at a triangle-boundary position.

Equations

• o.orientedEdge = (T.triangleBoundary o.fst).get o.snd

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.BoundaryPosition.edge {S : Type u_1} [TopologicalSpace S] {T : FiniteSurfaceTriangulation S} (o : T.BoundaryPosition) : T.Edge

The unoriented edge stored at a triangle-boundary position.

Equations

• o.edge = o.orientedEdge.edge

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.TriangleAdjacent {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f g : T.Triangle) : Prop

Two triangles are adjacent when their stored boundaries share an unoriented edge.

Equations

• T.TriangleAdjacent f g = ∃ df ∈ T.triangleBoundary f, ∃ dg ∈ T.triangleBoundary g, df.edge = dg.edge

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.IncidenceCertificate {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : Prop

Incidence information needed by the legacy triangulation-to-cell-complex bridge.

edge_valence_le_two is deliberately stated for boundary positions rather than merely named edges. This detects repeated uses inside one boundary word as well as uses by different triangles. The separate edge_used field is necessary because the legacy triangulation type can contain named edges which occur in no triangle boundary. Genuine geometric triangulations will discharge both fields from their generated two-vertex faces.

• triangle_nonempty : Nonempty T.Triangle
• boundary_rotated_injective (f g : T.Triangle) : T.triangleBoundary f ~r T.triangleBoundary g → f = g
• edge_used (e : T.Edge) : ∃ (o : T.BoundaryPosition), o.edge = e
• edge_valence_le_two (e : T.Edge) (o₀ o₁ o₂ : T.BoundaryPosition) : o₀.edge = e → o₁.edge = e → o₂.edge = e → o₀ = o₁ ∨ o₀ = o₂ ∨ o₁ = o₂
• dual_connected (f g : T.Triangle) : Relation.ReflTransGen T.TriangleAdjacent f g

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toIntrinsic {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Moise.IntrinsicTwoComplex

Forget the target-space homeomorphism and retain the intrinsic two-complex.

Equations

• T.toIntrinsic = { Vertex := T.Vertex, vertexFintype := T.vertexFintype, vertexDecidableEq := T.vertexDecidableEq, faces := T.faces, faces_card := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toIntrinsic_faces {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : T.toIntrinsic.faces = T.faces

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedEdgeSource {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : OrientedEdge T.Edge → T.Vertex

Source vertex of an oriented geometric edge.

Equations

• T.orientedEdgeSource (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos e) = T.edgeSource e
• T.orientedEdgeSource (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg e) = T.edgeTarget e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedEdgeTarget {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : OrientedEdge T.Edge → T.Vertex

Target vertex of an oriented geometric edge.

Equations

• T.orientedEdgeTarget (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.pos e) = T.edgeTarget e
• T.orientedEdgeTarget (LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.neg e) = T.edgeSource e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedFaceEdge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : ZMod 3) : OrientedEdge T.Edge

The globally named edge between two consecutive cyclic vertices of a face, signed so that its orientation follows the cyclic order of that face.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedFaceEdge_edge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : ZMod 3) : (T.orientedFaceEdge t i).edge = T.toIntrinsic.faceEdge t i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedFaceEdge_source {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : ZMod 3) : T.orientedEdgeSource (T.orientedFaceEdge t i) = T.toIntrinsic.faceVertex t i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedFaceEdge_target {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : ZMod 3) : T.orientedEdgeTarget (T.orientedFaceEdge t i) = T.toIntrinsic.faceVertex t (i + 1)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) : List (OrientedEdge T.Edge)

The cyclic signed boundary of a geometric triangle. Slot i traverses from the i-th cyclic face vertex to the next one.

Equations

• T.triangleBoundary t = List.ofFn fun (i : Fin 3) => T.orientedFaceEdge t ((ZMod.finEquiv 3) i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_length {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) : (T.triangleBoundary t).length = 3

Every cyclic triangle boundary has exactly three occurrences.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_get {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : Fin (T.triangleBoundary t).length) : (T.triangleBoundary t).get i = T.orientedFaceEdge t ((ZMod.finEquiv 3) (Fin.cast ⋯ i))

Reading a cyclic triangle boundary recovers the correspondingly indexed oriented face edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_get_edge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : Fin (T.triangleBoundary t).length) : ((T.triangleBoundary t).get i).edge = T.toIntrinsic.faceEdge t ((ZMod.finEquiv 3) (Fin.cast ⋯ i))

The underlying edge at a cyclic boundary position is the intrinsic edge with the same index.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_get_source {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : Fin (T.triangleBoundary t).length) : T.orientedEdgeSource ((T.triangleBoundary t).get i) = T.toIntrinsic.faceVertex t ((ZMod.finEquiv 3) (Fin.cast ⋯ i))

The source of a boundary occurrence is its cyclic face vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_get_target {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (i : Fin (T.triangleBoundary t).length) : T.orientedEdgeTarget ((T.triangleBoundary t).get i) = T.toIntrinsic.faceVertex t ((ZMod.finEquiv 3) (Fin.cast ⋯ i) + 1)

The target of a boundary occurrence is the next cyclic face vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edge_subset_of_mem_triangleBoundary {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) {t : T.Triangle} {oe : OrientedEdge T.Edge} (hoe : oe ∈ T.triangleBoundary t) : ↑oe.edge ⊆ ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.mem_map_edge_triangleBoundary_iff {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) (e : T.Edge) : e ∈ List.map OrientedEdge.edge (T.triangleBoundary t) ↔ ↑e ⊆ ↑t

A named geometric edge lies in the underlying triangle-boundary list exactly when it is a face of that triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_edge_get_injective {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) : Function.Injective fun (i : Fin (T.triangleBoundary t).length) => ((T.triangleBoundary t).get i).edge

Distinct cyclic positions in one face name distinct underlying edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangleBoundary_nodup {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) : (T.triangleBoundary t).Nodup

Each geometric edge occurs at most once in a triangle's canonical boundary list.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteSurfaceTriangulation {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : FiniteSurfaceTriangulation S

Package a geometric triangulation as the project's FiniteSurfaceTriangulation object.

This is the compatibility bridge: downstream consumers (the cell-complex conversion and the Gallier--Xu route) keep their interface, while the triangulation content now lives in the faithful geometric object.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteSurfaceTriangulation_homeomorphSurface {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Nonempty (T.toFiniteSurfaceTriangulation.realization ≃ₜ S)

The bridge realizes the ambient space.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.incidenceCertificate_of_surfaceIncidence {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (h : T.SurfaceIncidence) : T.toFiniteSurfaceTriangulation.IncidenceCertificate

A geometric surface-incidence certificate supplies every incidence obligation required by the legacy finite triangulation bridge.

theorem LeanEval.Topology.ClassificationOfSurfaces.moise_triangulation (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty (GeometricTriangulation S)

The compact bordered extension of Radó's theorem. Moise, Geometric Topology in Dimensions 2 and 3, Ch. 8, Thm. 3 proves the boundaryless case; the proof assembled here carries the same induction through half-disk charts while preserving the manifold-boundary stratum.

Every compact connected surface in the Eval sense admits a finite geometric triangulation — a homeomorphism onto the realization of a finite two-dimensional simplicial complex.

Semantic anchors: the conclusion implies CompactSpace S and T2Space S (GeometricTriangulation.compactSpace, GeometricTriangulation.t2Space), and is refuted for non-compact spaces (Moise/Countermodels.lean), so it cannot be discharged by a junk witness.

The proof is the assembled boundary-preserving Radó chart induction (Moise.moise_triangulation_of_boundaries).

theorem LeanEval.Topology.ClassificationOfSurfaces.moise_triangulation_explicit (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F : Finset (Finset V)), (∀ t ∈ F, t.card = 3) ∧ Nonempty (↑(GeometricRealization V F) ≃ₜ S)

Radó's theorem with its conclusion expanded into the finite vertex type, the family of three-vertex faces, and the homeomorphism from their barycentric realization. This is a definition-audit surface for moise_triangulation, not a second proof.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.compactEvalSurfaceGeometricTriangulation (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : GeometricTriangulation S

The named geometric triangulation produced for a compact connected Eval surface.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.compactEvalSurfaceGeometricTriangulation S = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_geometricTriangulation_surfaceIncidence (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : (compactEvalSurfaceGeometricTriangulation S).SurfaceIncidence

The Radó triangulation carries nonempty-face, edge-valence, and dual-connectivity data.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.compactEvalSurfaceFiniteSurfaceTriangulation (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : FiniteSurfaceTriangulation S

The named finite surface triangulation produced for a compact connected Eval surface, obtained from the geometric triangulation boundary moise_triangulation through the compatibility bridge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_finiteSurfaceTriangulation_incidenceCertificate (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : (compactEvalSurfaceFiniteSurfaceTriangulation S).IncidenceCertificate

The compatibility triangulation inherits the complete incidence certificate.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_finiteSurfaceTriangulation_homeomorphSurface (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty ((compactEvalSurfaceFiniteSurfaceTriangulation S).realization ≃ₜ S)

The named compact connected Eval surface triangulation realizes the ambient surface.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_finitely_triangulable (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : ∃ (T : FiniteSurfaceTriangulation S), Nonempty (T.realization ≃ₜ S)

Moise/PL theorem boundary: compact connected Eval surfaces admit finite triangulations.