Geometric triangulations

The faithful statement of "the space S admits a finite triangulation": S is homeomorphic to the geometric realization of a finite two-dimensional simplicial complex.

The realization is concrete: for a finite vertex type V and a finite family F of faces (3-element vertex sets), GeometricRealization V F is the subset of the standard simplex stdSimplex ℝ V consisting of points supported on some face. This is the classical geometric realization by barycentric coordinates; it is a compact Hausdorff polyhedron by construction, so the definition cannot be satisfied by junk witnesses (Empty face types, arbitrary realization fields, and so on): the homeomorphism type pins S to an actual finite union of geometric 2-simplexes.

Semantic anchors (see Moise/Countermodels.lean and the Definition Faithfulness section of docs/AUTOFORMALIZATION_GUIDE.md):

• must-imply: GeometricTriangulation.compactSpace, GeometricTriangulation.t2Space;
• positive example: the standard 2-simplex triangulates itself;
• non-example: ℝ and ℚ admit no geometric triangulation (they are not compact).

theorem IsPreconnected.transGen_of_finite_iUnion {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Finite ι] {s : ι → Set α} (hs : IsPreconnected (⋃ (n : ι), s n)) (hs' : ∀ (i : ι), IsClosed (s i)) (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) : Relation.TransGen (fun (a b : ι) => (s a ∩ s b).Nonempty) i j

A finite closed cover of a preconnected set has a connected intersection graph.

This is the closed-cover counterpart of IsPreconnected.transGen_of_iUnion, whose open-cover hypothesis is not available for the closed simplexes of a geometric realization.

def LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization (V : Type u_1) [Fintype V] (F : Finset (Finset V)) : Set (V → ℝ)

The geometric realization of a finite family F of faces on a finite vertex type V: the points of the standard simplex on V whose support lies inside some face of F. For a face t this carves out the geometric simplex spanned by t, so the realization is the finite union of the geometric simplexes of F, glued along shared barycentric-coordinate faces.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization V F = {x : V → ℝ | x ∈ stdSimplex ℝ V ∧ ∃ t ∈ F, ∀ v ∉ t, x v = 0}

def LeanEval.Topology.ClassificationOfSurfaces.GeometricFace (V : Type u_1) [Fintype V] (t : Finset V) : Set (V → ℝ)

The geometric simplex carried by one finite set of vertices.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.GeometricFace V t = {x : V → ℝ | x ∈ stdSimplex ℝ V ∧ ∀ v ∉ t, x v = 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricFace.inter {V : Type u_1} [Fintype V] [DecidableEq V] (t u : Finset V) : GeometricFace V t ∩ GeometricFace V u = GeometricFace V (t ∩ u)

Semantic anchor: two barycentric faces meet in exactly their common face.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricFace.nonempty_iff {V : Type u_1} [Fintype V] (t : Finset V) : (GeometricFace V t).Nonempty ↔ t.Nonempty

A barycentric face is nonempty exactly when it has a vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricFace.isClosed {V : Type u_1} [Fintype V] (t : Finset V) : IsClosed (GeometricFace V t)

Each barycentric face is closed in the ambient coordinate space.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.eq_biUnion_geometricFace {V : Type u_1} [Fintype V] {F : Finset (Finset V)} : GeometricRealization V F = ⋃ t ∈ F, GeometricFace V t

The global realization is literally the finite union of its geometric faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.subset_stdSimplex {V : Type u_1} [Fintype V] {F : Finset (Finset V)} : GeometricRealization V F ⊆ stdSimplex ℝ V

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.isClosed {V : Type u_1} [Fintype V] {F : Finset (Finset V)} : IsClosed (GeometricRealization V F)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.isCompact {V : Type u_1} [Fintype V] {F : Finset (Finset V)} : IsCompact (GeometricRealization V F)

instance LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.instCompactSpaceElemForallReal {V : Type u_1} [Fintype V] {F : Finset (Finset V)} : CompactSpace ↑(GeometricRealization V F)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.eq_empty_of_no_faces {V : Type u_1} [Fintype V] : GeometricRealization V ∅ = ∅

The realization of the empty face family is empty.

instance LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization.instIsEmptyElemForallRealEmptyCollectionFinset {V : Type u_1} [Fintype V] : IsEmpty ↑(GeometricRealization V ∅)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.Face {Vertex : Type u_1} (faces : Finset (Finset Vertex)) : Type u_1

A listed maximal face of a finite triangle family.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.Face faces = ↥faces

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.edges {Vertex : Type u_1} [DecidableEq Vertex] (faces : Finset (Finset Vertex)) : Finset (Finset Vertex)

The two-vertex faces occurring in a finite triangle family.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.edges faces = faces.biUnion fun (t : Finset Vertex) => Finset.powersetCard 2 t

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceAdjacent {Vertex : Type u_1} (faces : Finset (Finset Vertex)) (f g : Face faces) : Prop

Two listed triangles are dual-adjacent when they share a two-vertex face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceAdjacent faces f g = ∃ (e : Finset Vertex), e.card = 2 ∧ e ⊆ ↑f ∧ e ⊆ ↑g

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceAdjacentAtVertex {Vertex : Type u_1} (faces : Finset (Finset Vertex)) (v : Vertex) (f g : Face faces) : Prop

Two listed triangles are adjacent at v when they share a two-vertex face containing v.

Unlike FaceAdjacent, this relation remembers the vertex star in which the adjacency step occurs.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceAdjacentAtVertex faces v f g = ∃ (e : Finset Vertex), e.card = 2 ∧ v ∈ e ∧ e ⊆ ↑f ∧ e ⊆ ↑g

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceIntersects {Vertex : Type u_1} [DecidableEq Vertex] (faces : Finset (Finset Vertex)) (f g : Face faces) : Prop

Two listed triangles meet when their vertex sets have a common vertex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceIntersects faces f g = (↑f ∩ ↑g).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceAdjacent_symm {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {f g : Face faces} (h : FaceAdjacent faces f g) : FaceAdjacent faces g f

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceAdjacentAtVertex_symm {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : FaceAdjacentAtVertex faces v f g) : FaceAdjacentAtVertex faces v g f

Fixed-vertex face adjacency is symmetric.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceAdjacent_of_faceAdjacentAtVertex {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : FaceAdjacentAtVertex faces v f g) : FaceAdjacent faces f g

A fixed-vertex adjacency step is an ordinary dual-adjacency step.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.mem_left_of_faceAdjacentAtVertex {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : FaceAdjacentAtVertex faces v f g) : v ∈ ↑f

The left endpoint of a fixed-vertex adjacency step contains the fixed vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.mem_right_of_faceAdjacentAtVertex {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : FaceAdjacentAtVertex faces v f g) : v ∈ ↑g

The right endpoint of a fixed-vertex adjacency step contains the fixed vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.card_inter_le_one_of_not_faceAdjacent {Vertex : Type u_1} [DecidableEq Vertex] {faces : Finset (Finset Vertex)} {f g : Face faces} (h : ¬FaceAdjacent faces f g) : (↑f ∩ ↑g).card ≤ 1

Faces in different dual components share at most one vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.reflTransGen_faceAdjacent_symm {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {f g : Face faces} (h : Relation.ReflTransGen (FaceAdjacent faces) f g) : Relation.ReflTransGen (FaceAdjacent faces) g f

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.reflTransGen_faceAdjacent_of_faceAdjacentAtVertex {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : Relation.ReflTransGen (FaceAdjacentAtVertex faces v) f g) : Relation.ReflTransGen (FaceAdjacent faces) f g

A chain of fixed-vertex adjacency steps is an ordinary dual-adjacency chain.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.reflTransGen_faceAdjacentAtVertex_symm {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (h : Relation.ReflTransGen (FaceAdjacentAtVertex faces v) f g) : Relation.ReflTransGen (FaceAdjacentAtVertex faces v) g f

Fixed-vertex adjacency chains can be traversed in reverse.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.mem_of_reflTransGen_faceAdjacentAtVertex {Vertex : Type u_1} {faces : Finset (Finset Vertex)} {v : Vertex} {f g : Face faces} (hvf : v ∈ ↑f) (h : Relation.ReflTransGen (FaceAdjacentAtVertex faces v) f g) : v ∈ ↑g

Every endpoint reached from a face containing v through fixed-vertex adjacency still contains v.

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsDualConnected {Vertex : Type u_1} (faces : Finset (Finset Vertex)) : Prop

Every two listed triangles are connected by a finite chain of shared edges.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsVertexStarConnected {Vertex : Type u_1} (faces : Finset (Finset Vertex)) : Prop

Every pair of triangles incident to one vertex can be joined through shared edges.

For a triangulated surface this is the local connectedness assertion carried by the link of the vertex. This compatibility predicate does not require its intermediate faces to remain incident to that vertex; use IsStrongVertexStarConnected when that fixed-star invariant is needed.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsStrongVertexStarConnected {Vertex : Type u_1} (faces : Finset (Finset Vertex)) : Prop

Every pair of triangles incident to one vertex can be joined by a chain whose every adjacency step shares an edge containing that same vertex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsStrongVertexStarConnected.isVertexStarConnected {Vertex : Type u_1} {faces : Finset (Finset Vertex)} (hstar : IsStrongVertexStarConnected faces) : IsVertexStarConnected faces

Strong fixed-star connectivity implies the legacy vertex-star connectivity predicate.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.geometricFace_inter_nonempty_iff {Vertex : Type u_1} [DecidableEq Vertex] [Fintype Vertex] {faces : Finset (Finset Vertex)} (f g : Face faces) : (GeometricFace Vertex ↑f ∩ GeometricFace Vertex ↑g).Nonempty ↔ FaceIntersects faces f g

Geometric simplexes intersect exactly when their combinatorial faces share a vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isFaceIntersectionConnected_of_isPreconnected {Vertex : Type u_1} [DecidableEq Vertex] [Fintype Vertex] {faces : Finset (Finset Vertex)} (hface : ∀ (f : Face faces), (↑f).Nonempty) (hpre : IsPreconnected (GeometricRealization Vertex faces)) (f g : Face faces) : Relation.ReflTransGen (FaceIntersects faces) f g

Connectedness of a finite geometric realization connects all maximal faces through nonempty intersections.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsVertexStarConnected.isDualConnected {Vertex : Type u_1} [DecidableEq Vertex] {faces : Finset (Finset Vertex)} (hstar : IsVertexStarConnected faces) (hinter : ∀ (f g : Face faces), Relation.ReflTransGen (FaceIntersects faces) f g) : IsDualConnected faces

Connected vertex stars upgrade connectivity through arbitrary face intersections to connectivity through shared edges.

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfSubset {Vertex : Type u_1} {faces faces' : Finset (Finset Vertex)} (h : faces ⊆ faces') : Face faces → Face faces'

Regard a face of a subfamily as a face of a larger family.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfSubset h f = ⟨↑f, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfSubset_val {Vertex : Type u_1} {faces faces' : Finset (Finset Vertex)} (h : faces ⊆ faces') (f : Face faces) : ↑(faceOfSubset h f) = ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceAdjacent_faceOfSubset {Vertex : Type u_1} {faces faces' : Finset (Finset Vertex)} (h : faces ⊆ faces') {f g : Face faces} (hfg : FaceAdjacent faces f g) : FaceAdjacent faces' (faceOfSubset h f) (faceOfSubset h g)

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.reflTransGen_faceAdjacent_faceOfSubset {Vertex : Type u_1} {faces faces' : Finset (Finset Vertex)} (h : faces ⊆ faces') {f g : Face faces} (hfg : Relation.ReflTransGen (FaceAdjacent faces) f g) : Relation.ReflTransGen (FaceAdjacent faces') (faceOfSubset h f) (faceOfSubset h g)

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isDualConnected_union {Vertex : Type u_1} [DecidableEq Vertex] {left right : Finset (Finset Vertex)} (hleft : IsDualConnected left) (hright : IsDualConnected right) (fleft : Face left) (fright : Face right) (hcross : FaceAdjacent (left ∪ right) (faceOfSubset ⋯ fleft) (faceOfSubset ⋯ fright)) : IsDualConnected (left ∪ right)

Two dual-connected face families with a cross-adjacent pair have dual-connected union.

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.HasCrossEdge {Vertex : Type u_1} [DecidableEq Vertex] (left right : Finset (Finset Vertex)) : Prop

A face from each family shares a genuine two-vertex edge in the union family.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isDualConnected_union_of_hasCrossEdge {Vertex : Type u_1} [DecidableEq Vertex] {left right : Finset (Finset Vertex)} (hleft : IsDualConnected left) (hright : IsDualConnected right) (hcross : HasCrossEdge left right) : IsDualConnected (left ∪ right)

Two dual-connected face families with a shared cross-edge have dual-connected union.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isDualConnected_singleton {Vertex : Type u_1} (face : Finset Vertex) : IsDualConnected {face}

A face family consisting of one triangle is dual-connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isDualConnected_insert {Vertex : Type u_1} [DecidableEq Vertex] {faces : Finset (Finset Vertex)} (hfaces : IsDualConnected faces) (face : Finset Vertex) (anchor : Face faces) (hcross : FaceAdjacent (insert face faces) ⟨face, ⋯⟩ (faceOfSubset ⋯ anchor)) : IsDualConnected (insert face faces)

Adding a triangle along an edge of a dual-connected family preserves dual connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsStrongVertexStarConnected.isDualConnected {Vertex : Type u_1} [DecidableEq Vertex] {faces : Finset (Finset Vertex)} (hstar : IsStrongVertexStarConnected faces) (hinter : ∀ (f g : Face faces), Relation.ReflTransGen (FaceIntersects faces) f g) : IsDualConnected faces

Strong fixed-star connectivity supplies dual connectivity whenever the face-intersection graph is connected.

structure LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.SurfaceIncidence {Vertex : Type u_1} [DecidableEq Vertex] (faces : Finset (Finset Vertex)) : Prop

Incidence conditions making a finite family of triangles a connected pseudomanifold with boundary: it is nonempty, no edge has valence above two, and its dual graph is connected.

• faces_nonempty : faces.Nonempty
• edge_valence_le_two (e : Finset Vertex) : e ∈ edges faces → {t ∈ faces | e ⊆ t}.card ≤ 2
• dual_connected : IsDualConnected faces

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

A finite triangulation of the topological space S by geometric 2-simplexes: a finite vertex type, a finite family of 3-element faces, and a homeomorphism from the geometric realization of that family onto S.

There is no separate realization field to weaken: the realization is computed from the combinatorial data, so a GeometricTriangulation S exists only when S really is a finite two-dimensional polyhedron.

• Vertex : Type

  The (finite) vertex type of the triangulation.

• vertexFintype : Fintype self.Vertex

  The vertex type is finite.

• vertexDecidableEq : DecidableEq self.Vertex

  Vertices have decidable equality.

• faces : Finset (Finset self.Vertex)

  The faces: each is a set of vertices spanning a geometric 2-simplex.

• faces_card (t : Finset self.Vertex) : t ∈ self.faces → t.card = 3

  Every face has exactly three vertices, so the complex is purely two-dimensional.

• homeo : ↑(GeometricRealization self.Vertex self.faces) ≃ₜ S

  The geometric realization of the face family is homeomorphic to S.

theorem LeanEval.Topology.ClassificationOfSurfaces.nonempty_geometricTriangulation_iff_explicit {S : Type u_1} [TopologicalSpace S] : Nonempty (GeometricTriangulation S) ↔ ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F : Finset (Finset V)), (∀ t ∈ F, t.card = 3) ∧ Nonempty (↑(GeometricRealization V F) ≃ₜ S)

Expanded, independently inspectable form of GeometricTriangulation.

This theorem pins the public meaning of the structure: no realization or incidence data is hidden behind an additional field.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.SurfaceIncidence {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Prop

Surface-incidence certificate for a faithful geometric triangulation.

Equations

• T.SurfaceIncidence = LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.SurfaceIncidence T.faces

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.realization {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Set (T.Vertex → ℝ)

The realization of the triangulation, as a polyhedron in barycentric coordinates.

Equations

• T.realization = LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization T.Vertex T.faces

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.compactSpace {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : CompactSpace S

Must-imply anchor: a finitely triangulated space is compact. This is what rules out the empty/junk triangulations that satisfied the previous SurfaceTriangulable predicate.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.t2Space {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : T2Space S

Must-imply anchor: a finitely triangulated space is Hausdorff (the realization is a subspace of a finite product of lines).

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faces_nonempty {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [Nonempty S] : T.faces.Nonempty

A triangulation of a nonempty space has at least one two-dimensional face.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faces_isDualConnected_of_isVertexStarConnected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ConnectedSpace S] (hstar : TriangleFamily.IsVertexStarConnected T.faces) : TriangleFamily.IsDualConnected T.faces

On a connected realization, local edge-connectedness of every vertex star is enough to deduce global dual connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faces_isDualConnected_of_isStrongVertexStarConnected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ConnectedSpace S] (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) : TriangleFamily.IsDualConnected T.faces

On a connected realization, strong fixed-star connectivity also implies global dual connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.three_le_card_vertex {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [Nonempty S] : 3 ≤ Fintype.card T.Vertex

A triangulation of a nonempty space has at least three available vertices.

def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edges {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Finset (Finset T.Vertex)

The edges of the triangulation: the 2-element subsets of its faces.

Equations

• T.edges = T.faces.biUnion fun (t : Finset T.Vertex) => Finset.powersetCard 2 t

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.card_of_mem_edges {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) {e : Finset T.Vertex} (he : e ∈ T.edges) : e.card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.mem_edges_of_subset_face {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) {e t : Finset T.Vertex} (ht : t ∈ T.faces) (het : e ⊆ t) (he : e.card = 2) : e ∈ T.edges

@[reducible, inline]

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

The edge type of the triangulation.

Equations

• T.Edge = ↥T.edges

@[reducible, inline]

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

The triangle (face) type of the triangulation.

Equations

• T.Triangle = ↥T.faces

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edge_card {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : (↑e).card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.triangle_card {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (t : T.Triangle) : (↑t).card = 3

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

The chosen first endpoint of an edge.

Equations

• T.edgeSource e = ⋯.choose

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

The chosen second endpoint of an edge.

Equations

• T.edgeTarget e = ⋯.choose

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edgeSource_ne_edgeTarget {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : T.edgeSource e ≠ T.edgeTarget e

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edge_eq_pair {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : ↑e = {T.edgeSource e, T.edgeTarget e}

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edgeSource_mem {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : T.edgeSource e ∈ ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.edgeTarget_mem {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : T.edgeTarget e ∈ ↑e

def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.IsBoundaryEdge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (e : T.Edge) : Prop

An edge is a boundary edge when it lies in exactly one face.

Equations

• T.IsBoundaryEdge e = ({t ∈ T.faces | ↑e ⊆ t}.card = 1)