Locally finite triangle complexes

Rado's induction in Moise Chapter 8 passes through locally finite, usually noncompact, PL complexes. Requiring every intermediate complex to be finite loses the frontier-vanishing construction used in the induction step. This file provides the corresponding ambient API while keeping the existing finite GeometricTriangulation as the final output.

A face is parametrized by the standard simplex on its three global vertices. The faceMap_eq_iff field says both that parametrizations agree on common faces and that distinct geometric points are never identified. Thus the structure records the full face-to-face condition, rather than only a family of carriers. Local finiteness is imposed on the carrier family in the ambient topology.

The main result is LocallyFiniteTriangleComplex.toGeometricTriangulation: on a compact Hausdorff space, local finiteness makes the face type finite; the no-junk-vertices condition then makes the vertex type finite, and finite closed pasting produces the required homeomorphism from the canonical barycentric realization.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.extendFaceCoordinates {V : Type u_1} [DecidableEq V] (t : Finset V) (x : ↑(stdSimplex ℝ ↥t)) : V → ℝ

Extend barycentric coordinates on a finite face by zero to the global vertex type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.extendFaceCoordinates t x v = if hv : v ∈ t then x ⟨v, hv⟩ else 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.extendFaceCoordinates_of_mem {V : Type u_1} [DecidableEq V] (t : Finset V) (x : ↑(stdSimplex ℝ ↥t)) {v : V} (hv : v ∈ t) : extendFaceCoordinates t x v = x ⟨v, hv⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.extendFaceCoordinates_of_notMem {V : Type u_1} [DecidableEq V] (t : Finset V) (x : ↑(stdSimplex ℝ ↥t)) {v : V} (hv : v ∉ t) : extendFaceCoordinates t x v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stdSimplex_map_subtypeVal_eq_extendFaceCoordinates {V : Type u_1} [Fintype V] [DecidableEq V] (t : Finset V) (x : ↑(stdSimplex ℝ ↥t)) : ⇑(stdSimplex.map Subtype.val x) = extendFaceCoordinates t x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.extendFaceCoordinates_map_subset {V : Type u_1} [DecidableEq V] {e t : Finset V} (het : e ⊆ t) (x : ↑(stdSimplex ℝ ↥e)) : extendFaceCoordinates t (stdSimplex.map (fun (v : ↥e) => ⟨↑v, ⋯⟩) x) = extendFaceCoordinates e x

Relabeling a finite face along an embedding

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMapSubtypeEquiv {A : Type u_1} {B : Type u_2} (e : A ↪ B) (t : Finset A) : ↥t ≃ ↥(Finset.map e t)

The vertices of a finite face are equivalent to the vertices of its image under an embedding.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMapSubtypeEquiv e t = Equiv.ofBijective (fun (a : ↥t) => ⟨e ↑a, ⋯⟩) ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMapSubtypeEquiv_apply_val {A : Type u_1} {B : Type u_2} (e : A ↪ B) (t : Finset A) (a : ↥t) : ↑((finsetMapSubtypeEquiv e t) a) = e ↑a

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceSimplex {A : Type u_1} {B : Type u_2} (e : A ↪ B) (t : Finset A) (x : ↑(stdSimplex ℝ ↥(Finset.map e t))) : ↑(stdSimplex ℝ ↥t)

Pull simplex coordinates on a relabeled face back to the original face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceSimplex e t x = stdSimplex.map (⇑(LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMapSubtypeEquiv e t).symm) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceSimplex_surjective {A : Type u_1} {B : Type u_2} (e : A ↪ B) (t : Finset A) : Function.Surjective (relabelFaceSimplex e t)

Face relabeling along an embedding is onto.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceSimplex_extended_apply {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (e : A ↪ B) (t : Finset A) (x : ↑(stdSimplex ℝ ↥(Finset.map e t))) (a : A) : extendFaceCoordinates t (relabelFaceSimplex e t x) a = extendFaceCoordinates (Finset.map e t) x (e a)

Pulling coordinates back along a face relabeling preserves the coordinate at every original vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceSimplex_extended_eq_iff {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (e : A ↪ B) {s t : Finset A} {x : ↑(stdSimplex ℝ ↥(Finset.map e s))} {y : ↑(stdSimplex ℝ ↥(Finset.map e t))} : extendFaceCoordinates s (relabelFaceSimplex e s x) = extendFaceCoordinates t (relabelFaceSimplex e t y) ↔ extendFaceCoordinates (Finset.map e s) x = extendFaceCoordinates (Finset.map e t) y

Relabeling two faces by the same embedding preserves equality of their global zero-extended coordinate functions.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.sum_extendFaceCoordinates_relabelFaceSimplex {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (e : A ↪ B) (t : Finset A) (x : ↑(stdSimplex ℝ ↥(Finset.map e t))) (F : B → ℝ) : ∑ b : B, extendFaceCoordinates (Finset.map e t) x b * F b = ∑ a : A, extendFaceCoordinates t (relabelFaceSimplex e t x) a * F (e a)

Relabeling does not change a weighted evaluation of the zero-extended coordinates.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.univMapSubtypeEquiv {A : Type u_1} {B : Type u_2} [Fintype A] (e : A ↪ B) : ↥(Finset.map e Finset.univ) ≃ A

When the source face is the whole finite type, remove the vacuous membership subtype after pulling coordinates back along an embedding.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelUnivSimplex {A : Type u_1} {B : Type u_2} [Fintype A] (e : A ↪ B) (x : ↑(stdSimplex ℝ ↥(Finset.map e Finset.univ))) : ↑(stdSimplex ℝ A)

Pull simplex coordinates on the image of a finite type back to that finite type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelUnivSimplex e x = stdSimplex.map (⇑(LeanEval.Topology.ClassificationOfSurfaces.Moise.univMapSubtypeEquiv e)) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelUnivSimplex_surjective {A : Type u_1} {B : Type u_2} [Fintype A] (e : A ↪ B) : Function.Surjective (relabelUnivSimplex e)

Pullback along an embedded whole finite vertex type is onto: its inverse simply pushes coordinates forward along the inverse equivalence onto the image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelUnivSimplex_apply {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq B] (e : A ↪ B) (x : ↑(stdSimplex ℝ ↥(Finset.map e Finset.univ))) (a : A) : (relabelUnivSimplex e x) a = extendFaceCoordinates (Finset.map e Finset.univ) x (e a)

The whole-type relabeling preserves the coordinate of every embedded source vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stdSimplex_map_embedding_apply {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (e : A ↪ B) (x : ↑(stdSimplex ℝ A)) (a : A) : (stdSimplex.map (⇑e) x) (e a) = x a

An injective vertex map preserves the coordinate at each source vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stdSimplex_map_embedding_apply_of_notMem_range {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (e : A ↪ B) (x : ↑(stdSimplex ℝ A)) {b : B} (hb : b ∉ Set.range ⇑e) : (stdSimplex.map (⇑e) x) b = 0

An injective vertex map has zero coordinate away from its image.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceFamily {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : Finset (Finset B)

Relabel a finite face family along an embedding of its vertex type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelFaceFamily e F = Finset.image (fun (t : Finset A) => Finset.map e t) F

def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfRelabel {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) {faces : Finset (Finset A)} : Face faces → Face (Moise.relabelFaceFamily e faces)

Regard a listed face as a face of the family obtained by injectively relabeling its vertices.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfRelabel e f = ⟨Finset.map e ↑f, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceOfRelabel_val {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) {faces : Finset (Finset A)} (f : Face faces) : ↑(faceOfRelabel e f) = Finset.map e ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceAdjacent_faceOfRelabel {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) {faces : Finset (Finset A)} {f g : Face faces} (hfg : FaceAdjacent faces f g) : FaceAdjacent (Moise.relabelFaceFamily e faces) (faceOfRelabel e f) (faceOfRelabel e g)

Injective vertex relabeling preserves dual adjacency of listed faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.reflTransGen_faceAdjacent_faceOfRelabel {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) {faces : Finset (Finset A)} {f g : Face faces} (hfg : Relation.ReflTransGen (FaceAdjacent faces) f g) : Relation.ReflTransGen (FaceAdjacent (Moise.relabelFaceFamily e faces)) (faceOfRelabel e f) (faceOfRelabel e g)

Injective vertex relabeling carries a finite dual path to the relabeled family.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.isDualConnected_relabel {A : Type u_1} {B : Type u_2} [DecidableEq B] (e : A ↪ B) {faces : Finset (Finset A)} (hfaces : IsDualConnected faces) : IsDualConnected (Moise.relabelFaceFamily e faces)

Dual connectivity is preserved by an injective relabeling of the vertex type.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.hasCrossEdge_relabel_of_mapped_edge_eq {A : Type u_1} {B : Type u_2} {C : Type u_3} [DecidableEq C] (eleft : A ↪ C) (eright : B ↪ C) {left : Finset (Finset A)} {right : Finset (Finset B)} (fleft : Face left) (fright : Face right) (edgeLeft : Finset A) (edgeRight : Finset B) (hedgeCard : edgeLeft.card = 2) (hedgeLeft : edgeLeft ⊆ ↑fleft) (hedgeRight : edgeRight ⊆ ↑fright) (hmap : Finset.map eleft edgeLeft = Finset.map eright edgeRight) : HasCrossEdge (Moise.relabelFaceFamily eleft left) (Moise.relabelFaceFamily eright right)

Faces relabeled from different vertex types share an edge when the two source edges have the same relabeled image.

theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.hasCrossEdge_relabel {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (e : A ↪ B) {left right : Finset (Finset A)} (hcross : HasCrossEdge left right) : HasCrossEdge (Moise.relabelFaceFamily e left) (Moise.relabelFaceFamily e right)

A shared edge remains a shared edge when both families are injectively relabeled.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : ↑(GeometricRealization A F) → ↑(GeometricRealization B (relabelFaceFamily e F))

Push a geometric realization forward along an injective relabeling of all vertices.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization e F x = ⟨⇑(stdSimplex.map ⇑e ⟨↑x, ⋯⟩), ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.pullGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : ↑(GeometricRealization B (relabelFaceFamily e F)) → ↑(GeometricRealization A F)

Pull a point of a relabeled realization back to its original vertex type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.pullGeometricRealization e F y = ⟨fun (a : A) => ↑y (e a), ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization_val {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (x : ↑(GeometricRealization A F)) : ↑(pushGeometricRealization e F x) = ⇑(stdSimplex.map ⇑e ⟨↑x, ⋯⟩)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization_apply_embedding {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (x : ↑(GeometricRealization A F)) (a : A) : ↑(pushGeometricRealization e F x) (e a) = ↑x a

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization_apply_of_notMem_range {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (x : ↑(GeometricRealization A F)) {b : B} (hb : b ∉ Set.range ⇑e) : ↑(pushGeometricRealization e F x) b = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pushGeometricRealization_val_eq_of_val_eq {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F G : Finset (Finset A)) (x : ↑(GeometricRealization A F)) (y : ↑(GeometricRealization A G)) (hxy : ↑x = ↑y) : ↑(pushGeometricRealization e F x) = ↑(pushGeometricRealization e G y)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pullGeometricRealization_apply {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (y : ↑(GeometricRealization B (relabelFaceFamily e F))) (a : A) : ↑(pullGeometricRealization e F y) a = ↑y (e a)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.pull_pushGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (x : ↑(GeometricRealization A F)) : pullGeometricRealization e F (pushGeometricRealization e F x) = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.push_pullGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) (y : ↑(GeometricRealization B (relabelFaceFamily e F))) : pushGeometricRealization e F (pullGeometricRealization e F y) = y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_pushGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : Continuous (pushGeometricRealization e F)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_pullGeometricRealization {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : Continuous (pullGeometricRealization e F)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.relabelGeometricRealizationHomeomorph {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (F : Finset (Finset A)) : ↑(GeometricRealization A F) ≃ₜ ↑(GeometricRealization B (relabelFaceFamily e F))

Relabeling a finite face family along a vertex embedding does not change its realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.sum_extendFaceCoordinates_relabelUnivSimplex {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (e : A ↪ B) (x : ↑(stdSimplex ℝ ↥(Finset.map e Finset.univ))) (F : B → ℝ) : ∑ b : B, extendFaceCoordinates (Finset.map e Finset.univ) x b * F b = ∑ a : A, (relabelUnivSimplex e x) a * F (e a)

Weighted evaluation is unchanged by whole-type relabeling.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.sum_attach_mul_eq_sum_extendFaceCoordinates {V : Type u_1} [DecidableEq V] (t : Finset V) (x : ↑(stdSimplex ℝ ↥t)) (F : V → ℝ) : ∑ v : ↥t, x v * F ↑v = ∑ v ∈ t, extendFaceCoordinates t x v * F v

A sum over the subtype of a finite face is the corresponding sum of its zero-extended coordinates over the underlying vertex set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.sum_extendFaceCoordinates_eq_of_eq {V : Type u_1} [DecidableEq V] {s t : Finset V} (x : ↑(stdSimplex ℝ ↥s)) (y : ↑(stdSimplex ℝ ↥t)) (hxy : extendFaceCoordinates s x = extendFaceCoordinates t y) (F : V → ℝ) : ∑ v : ↥s, x v * F ↑v = ∑ v : ↥t, y v * F ↑v

Equal zero-extended coordinates give equal weighted sums against any scalar-valued function on the global vertex type.

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

A locally finite family of parametrized triangles in an ambient topological space.

vertex_used excludes irrelevant vertices. This matters in the compactness-to-finiteness bridge: local finiteness controls the number of nonempty faces, and every vertex must then occur in one of those faces.

• Vertex : Type

  Global vertices, shared literally by incident faces.

• vertexDecidableEq : DecidableEq self.Vertex

  Equality of vertices is decidable so that faces are finite sets.

• Face : Type

  Maximal two-dimensional faces.

• faceDecidableEq : DecidableEq self.Face

  Equality of maximal faces is decidable.

• faceVertices : self.Face → Finset self.Vertex

  The three global vertices of a maximal face.

• faceVertices_card (f : self.Face) : (self.faceVertices f).card = 3

  Every maximal face is a triangle.

• vertex_used (v : self.Vertex) : ∃ (f : self.Face), v ∈ self.faceVertices f

  Every declared global vertex occurs in a maximal face.

• faceMap (f : self.Face) : ↑(stdSimplex ℝ ↥(self.faceVertices f)) → S

  Coordinate map of a closed triangle into the ambient space.

• faceMap_continuous (f : self.Face) : Continuous (self.faceMap f)

  Each coordinate map is continuous.

• faceMap_eq_iff {f g : self.Face} {x : ↑(stdSimplex ℝ ↥(self.faceVertices f))} {y : ↑(stdSimplex ℝ ↥(self.faceVertices g))} : self.faceMap f x = self.faceMap g y ↔ extendFaceCoordinates (self.faceVertices f) x = extendFaceCoordinates (self.faceVertices g) y

  Exact face-to-face compatibility and global injectivity, expressed in barycentric coordinates.

• locallyFinite : LocallyFinite fun (f : self.Face) => Set.range (self.faceMap f)

  The closed triangle carriers form a locally finite family.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Set S

The ambient carrier of one maximal face.

Equations

• K.faceCarrier f = Set.range (K.faceMap f)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.support {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : Set S

The ambient support of the locally finite complex.

Equations

• K.support = ⋃ (f : K.Face), K.faceCarrier f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceCarrier_nonempty {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : (K.faceCarrier f).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Function.Injective (K.faceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isEmbedding_faceMap {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (f : K.Face) : Topology.IsEmbedding (K.faceMap f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isCompact_faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : IsCompact (K.faceCarrier f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isClosed_faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (f : K.Face) : IsClosed (K.faceCarrier f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isClosed_support {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] : IsClosed K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.extendFaceCoordinates_vertex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) {v : K.Vertex} (hv : v ∈ K.faceVertices f) : extendFaceCoordinates (K.faceVertices f) (stdSimplex.vertex ⟨v, hv⟩) = Pi.single v 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.incidentFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : K.Face

A chosen maximal face incident to a global vertex.

Equations

• K.incidentFace v = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_faceVertices_incidentFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : v ∈ K.faceVertices (K.incidentFace v)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : S

The ambient point represented by a global vertex.

Equations

• K.vertexPoint v = K.faceMap (K.incidentFace v) (stdSimplex.vertex ⟨v, ⋯⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_vertex_eq_vertexPoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) {v : K.Vertex} (hv : v ∈ K.faceVertices f) : K.faceMap f (stdSimplex.vertex ⟨v, hv⟩) = K.vertexPoint v

Every incident face parametrization sends a shared abstract vertex to the same ambient point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_in_faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) {v : K.Vertex} (hv : v ∈ K.faceVertices f) : K.vertexPoint v ∈ K.faceCarrier f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : Function.Injective K.vertexPoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.locallyFinite_vertexPoints {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : LocallyFinite fun (v : K.Vertex) => {K.vertexPoint v}

Singleton carriers of the global vertices form a locally finite family.

Cyclic data on a maximal face

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexEquiv {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Fin 3 ≃ ↥(K.faceVertices f)

A chosen cyclic enumeration of the three vertices of a maximal face.

Equations

• K.faceVertexEquiv f = Fintype.equivOfCardEq ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.Vertex

Cyclically indexed vertices of a maximal face.

Equations

• K.faceVertex f i = ↑((K.faceVertexEquiv f) ((ZMod.finEquiv 3).symm i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertex_mem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.faceVertex f i ∈ K.faceVertices f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertex_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Function.Injective (K.faceVertex f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertex_ne_next {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.faceVertex f i ≠ K.faceVertex f (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertex_ne_add_two {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.faceVertex f i ≠ K.faceVertex f (i + 2)

Edges

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.IsEdge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : Finset K.Vertex) : Prop

A two-element vertex set contained in a maximal face.

Equations

• K.IsEdge e = (e.card = 2 ∧ ∃ (f : K.Face), e ⊆ K.faceVertices f)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.Edge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : Type

The edge type of a locally finite triangle complex.

Equations

• K.Edge = { e : Finset K.Vertex // K.IsEdge e }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFirst {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.Vertex

The chosen first endpoint of an edge.

Equations

• K.edgeFirst e = ⋯.choose

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSecond {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.Vertex

The chosen second endpoint of an edge.

Equations

• K.edgeSecond e = ⋯.choose

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFirst_ne_edgeSecond {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeFirst e ≠ K.edgeSecond e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edge_eq_pair {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : ↑e = {K.edgeFirst e, K.edgeSecond e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFirst_mem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeFirst e ∈ ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSecond_mem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeSecond e ∈ ↑e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.Edge

The edge joining two consecutive cyclic vertices of a maximal face.

Equations

• K.faceEdge f i = ⟨{K.faceVertex f i, K.faceVertex f (i + 1)}, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_val {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : ↑(K.faceEdge f i) = {K.faceVertex f i, K.faceVertex f (i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_inter_next {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : ↑(K.faceEdge f i) ∩ ↑(K.faceEdge f (i + 1)) = {K.faceVertex f (i + 1)}

Consecutive face edges share exactly their common cyclic vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_ne_next {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.faceEdge f i ≠ K.faceEdge f (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_endpoint_order {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.edgeFirst (K.faceEdge f i) = K.faceVertex f i ∧ K.edgeSecond (K.faceEdge f i) = K.faceVertex f (i + 1) ∨ K.edgeFirst (K.faceEdge f i) = K.faceVertex f (i + 1) ∧ K.edgeSecond (K.faceEdge f i) = K.faceVertex f i

The arbitrary endpoint ordering of a cyclic face edge is one of its two cyclic orientations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑(stdSimplex ℝ ↥↑e)

The standard one-simplex point at interval parameter r.

Equations

• K.edgeSimplexPath e r = ⟨(AffineMap.lineMap ⇑(stdSimplex.vertex ⟨K.edgeFirst e, ⋯⟩) ⇑(stdSimplex.vertex ⟨K.edgeSecond e, ⋯⟩)) ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_edgeSimplexPath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Continuous (K.edgeSimplexPath e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath_apply_first {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : (K.edgeSimplexPath e r) ⟨K.edgeFirst e, ⋯⟩ = 1 - ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath_apply_second {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : (K.edgeSimplexPath e r) ⟨K.edgeSecond e, ⋯⟩ = ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Function.Injective (K.edgeSimplexPath e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.Face

A chosen maximal face incident to an edge.

Equations

• K.edgeFace e = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edge_subset_faceVertices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : ↑e ⊆ K.faceVertices (K.edgeFace e)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeVertexToFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : ↥↑e → ↥(K.faceVertices (K.edgeFace e))

Include edge-local vertices into a chosen incident maximal face.

Equations

• K.edgeVertexToFace e v = ⟨↑v, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.extendFaceCoordinates_map_edgeVertexToFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (x : ↑(stdSimplex ℝ ↥↑e)) : extendFaceCoordinates (K.faceVertices (K.edgeFace e)) (stdSimplex.map (K.edgeVertexToFace e) x) = extendFaceCoordinates (↑e) x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMap {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (x : ↑(stdSimplex ℝ ↥↑e)) : S

Parametrization of a closed edge by its standard one-simplex.

Equations

• K.edgeMap e x = K.faceMap (K.edgeFace e) (stdSimplex.map (K.edgeVertexToFace e) x)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : S

The canonical interval parametrization of an ambient edge carrier.

Equations

• K.edgePath e r = K.edgeMap e (K.edgeSimplexPath e r)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMap_eq_faceMap {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (f : K.Face) (hef : ↑e ⊆ K.faceVertices f) (x : ↑(stdSimplex ℝ ↥↑e)) : K.edgeMap e x = K.faceMap f (stdSimplex.map (fun (v : ↥↑e) => ⟨↑v, ⋯⟩) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_edgeMap {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Continuous (K.edgeMap e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_edgePath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Continuous (K.edgePath e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMap_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Function.Injective (K.edgeMap e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePath_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Function.Injective (K.edgePath e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_edgeSimplexPath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Set.range (K.edgeSimplexPath e) = Set.univ

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Set S

The ambient carrier of an edge.

Equations

• K.edgeCarrier e = Set.range (K.edgeMap e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_edgePath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Set.range (K.edgePath e) = K.edgeCarrier e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMap_vertex_eq_vertexPoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (v : ↥↑e) : K.edgeMap e (stdSimplex.vertex v) = K.vertexPoint ↑v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier_inter_subset_sharedVertices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) {e d : K.Edge} (hed : e ≠ d) : K.edgeCarrier e ∩ K.edgeCarrier d ⊆ {p : S | ∃ v ∈ ↑e, v ∈ ↑d ∧ p = K.vertexPoint v}

Distinct edge carriers meet only at points represented by their shared abstract vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier_inter_eq_sharedVertices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) {e d : K.Edge} (hed : e ≠ d) : K.edgeCarrier e ∩ K.edgeCarrier d = {p : S | ∃ v ∈ ↑e, v ∈ ↑d ∧ p = K.vertexPoint v}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isCompact_edgeCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : IsCompact (K.edgeCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier_subset_faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeCarrier e ⊆ K.faceCarrier (K.edgeFace e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.locallyFinite_edgeCarriers {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : LocallyFinite K.edgeCarrier

Edge carriers inherit local finiteness from the maximal-face carriers.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath_zero {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeSimplexPath e ⟨0, ⋯⟩ = stdSimplex.vertex ⟨K.edgeFirst e, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexPath_one {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeSimplexPath e ⟨1, ⋯⟩ = stdSimplex.vertex ⟨K.edgeSecond e, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePath_zero {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgePath e ⟨0, ⋯⟩ = K.vertexPoint (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePath_one {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgePath e ⟨1, ⋯⟩ = K.vertexPoint (K.edgeSecond e)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.oneSkeleton {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : Set S

The one-skeleton carrier of a locally finite triangle complex.

Equations

• K.oneSkeleton = ⋃ (e : K.Edge), K.edgeCarrier e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier_subset_oneSkeleton {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeCarrier e ⊆ K.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.locallyFinite_oneSkeleton_cover {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : LocallyFinite K.edgeCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeParameter {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (p : S) (hp : p ∈ K.edgeCarrier e) : ↑(Set.Icc 0 1)

The canonical interval parameter of a point known to lie on an edge carrier.

Equations

• K.edgeParameter e p hp = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePath_edgeParameter {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (p : S) (hp : p ∈ K.edgeCarrier e) : K.edgePath e (K.edgeParameter e p hp) = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeParameter_unique {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) (p : S) (hp : p ∈ K.edgeCarrier e) (r : ↑(Set.Icc 0 1)) (hr : K.edgePath e r = p) : K.edgeParameter e p hp = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_mem_edgeCarrier_iff {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) (e : K.Edge) : K.vertexPoint v ∈ K.edgeCarrier e ↔ v ∈ ↑e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeParameter_vertexPoint_first {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeParameter e (K.vertexPoint (K.edgeFirst e)) ⋯ = ⟨0, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeParameter_vertexPoint_second {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : K.edgeParameter e (K.vertexPoint (K.edgeSecond e)) ⋯ = ⟨1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.disjoint_vertexPoint_edgeCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) {v : K.Vertex} {e : K.Edge} (hve : v ∉ ↑e) : Disjoint {K.vertexPoint v} (K.edgeCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isClosed_edgeCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (e : K.Edge) : IsClosed (K.edgeCarrier e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathToCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : ↑(Set.Icc 0 1) → ↑(K.edgeCarrier e)

The interval parametrization with codomain restricted to the edge carrier.

Equations

• K.edgePathToCarrier e r = ⟨K.edgePath e r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_edgePathToCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Continuous (K.edgePathToCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathToCarrier_injective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Function.Injective (K.edgePathToCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathToCarrier_surjective {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Function.Surjective (K.edgePathToCarrier e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathHomeomorph {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (e : K.Edge) : ↑(Set.Icc 0 1) ≃ₜ ↑(K.edgeCarrier e)

Every closed edge carrier is canonically homeomorphic to the unit interval.

Equations

• K.edgePathHomeomorph e = ⋯.toHomeomorphOfSurjective ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathHomeomorph_apply {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑((K.edgePathHomeomorph e) r) = K.edgePath e r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgePathHomeomorph_symm_val {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (e : K.Edge) (p : ↑(K.edgeCarrier e)) : K.edgePath e ((K.edgePathHomeomorph e).symm p) = ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isClosed_iUnion_edgeCarrier_notMem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [T2Space S] (v : K.Vertex) : IsClosed (⋃ (e : { e : K.Edge // v ∉ ↑e }), K.edgeCarrier ↑e)

The union of all edges not incident to a fixed vertex is closed.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_not_mem_iUnion_edgeCarrier_notMem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : K.vertexPoint v ∉ ⋃ (e : { e : K.Edge // v ∉ ↑e }), K.edgeCarrier ↑e

@[implicit_reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceFintype {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Fintype K.Face

Local finiteness on a compact ambient space makes the type of maximal faces finite.

Equations

• K.faceFintype = ⋯.fintypeOfCompact ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.finite_vertex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] : Finite K.Vertex

If the face type is finite and every vertex is used, then the global vertex type is finite.

@[implicit_reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexFintype {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Fintype K.Vertex

The finite vertex instance induced by compactness and the no-junk-vertices condition.

Equations

• K.vertexFintype = Fintype.ofFinite K.Vertex

@[instance_reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactFaceFintype {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Fintype K.Face

The compactFaceFintype declaration.

Equations

• K.compactFaceFintype = K.faceFintype

@[instance_reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactVertexFintype {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Fintype K.Vertex

The compactVertexFintype declaration.

Equations

• K.compactVertexFintype = K.vertexFintype

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactIntrinsic {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : IntrinsicTwoComplex

The finite intrinsic complex obtained from a compact locally finite triangle complex.

Equations

• K.compactIntrinsic = { Vertex := K.Vertex, vertexFintype := K.vertexFintype, vertexDecidableEq := K.vertexDecidableEq, faces := Finset.image K.faceVertices Finset.univ, faces_card := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactIntrinsic_faces {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : K.compactIntrinsic.faces = Finset.image K.faceVertices Finset.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactIntrinsic_face_mem {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (f : K.Face) : K.faceVertices f ∈ K.compactIntrinsic.faces

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.restrictToFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Fintype K.Vertex] (t : Finset K.Vertex) (x : ↑(stdSimplex ℝ K.Vertex)) (hx : ∀ v ∉ t, x v = 0) : ↑(stdSimplex ℝ ↥t)

Restrict a global standard-simplex point supported on t to the coordinates indexed by t.

Equations

• K.restrictToFace t x hx = ⟨fun (v : ↥t) => x ↑v, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.extendFaceCoordinates_restrictToFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Fintype K.Vertex] (t : Finset K.Vertex) (x : ↑(stdSimplex ℝ K.Vertex)) (hx : ∀ v ∉ t, x v = 0) : extendFaceCoordinates t (K.restrictToFace t x hx) = ⇑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_containingFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (x : K.compactIntrinsic.realization) : ∃ (f : K.Face), ∀ v ∉ K.faceVertices f, ↑x v = 0

Every point of the compact realization is supported on one of the original maximal faces.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.containingFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (x : K.compactIntrinsic.realization) : K.Face

A canonical maximal face containing a point of the compact realization.

Equations

• K.containingFace x = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supported_on_containingFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (x : K.compactIntrinsic.realization) (v : K.Vertex) : v ∉ K.faceVertices (K.containingFace x) → ↑x v = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactEval {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (x : K.compactIntrinsic.realization) : S

Evaluation of the compact barycentric realization through the locally finite face maps.

Equations

• K.compactEval x = K.faceMap (K.containingFace x) (K.restrictToFace (K.faceVertices (K.containingFace x)) ⟨↑x, ⋯⟩ ⋯)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.compactEval_eq_faceMap {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] (f : K.Face) (x : K.compactIntrinsic.realization) (hx : ∀ v ∉ K.faceVertices f, ↑x v = 0) : K.compactEval x = K.faceMap f (K.restrictToFace (K.faceVertices f) ⟨↑x, ⋯⟩ hx)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_compactEval {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Continuous K.compactEval

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.injective_compactEval {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Function.Injective K.compactEval

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.range_compactEval {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] : Set.range K.compactEval = K.support

The compact evaluation has exactly the ambient support of the locally finite complex as its range.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.toGeometricTriangulation {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [CompactSpace S] [T2Space S] (hcovers : K.support = Set.univ) : GeometricTriangulation S

A locally finite triangle complex covering a compact Hausdorff space is an honest finite geometric triangulation.

Equations

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

Finite complexes on their own support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.onSupport {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] : LocallyFiniteTriangleComplex ↑K.support

Regard a finite ambient triangle complex as a complex whose ambient space is exactly its support. This is the finite gluing bridge used in the Rado induction: once a compatible finite family of old and new triangles has been assembled, no separate ambient coverage proof is needed.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.onSupport_faceVertices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] (f : K.Face) : K.onSupport.faceVertices f = K.faceVertices f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.onSupport_faceMap_val {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] (f : K.Face) (x : ↑(stdSimplex ℝ ↥(K.faceVertices f))) : ↑(K.onSupport.faceMap f x) = K.faceMap f x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.onSupport_support {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] : K.onSupport.support = Set.univ

The support-restricted complex covers its ambient support subtype.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isCompact_support_of_finite {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] : IsCompact K.support

A finite ambient triangle complex has compact support, independently of compactness of the ambient space.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.finiteSupportGeometricTriangulation {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] [T2Space S] : GeometricTriangulation ↑K.support

A finite compatible triangle family triangulates its own support.

Equations

• K.finiteSupportGeometricTriangulation = K.onSupport.toGeometricTriangulation ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardMap (K : IntrinsicTwoComplex) (t : K.Face) (x : ↑(stdSimplex ℝ ↥↑t)) : K.realization

Include the standard simplex on one maximal face into the global barycentric realization.

Equations

• K.faceStandardMap t x = ⟨⇑(stdSimplex.map Subtype.val x), ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictToFaceSimplex (K : IntrinsicTwoComplex) (t : K.Face) (x : K.realization) (hx : ∀ v ∉ ↑t, ↑x v = 0) : ↑(stdSimplex ℝ ↥↑t)

Restrict an intrinsic realization point supported on one maximal face to that face's standard simplex.

Equations

• K.restrictToFaceSimplex t x hx = ⟨fun (v : ↥↑t) => ↑x ↑v, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardMap_val (K : IntrinsicTwoComplex) (t : K.Face) (x : ↑(stdSimplex ℝ ↥↑t)) : ↑(K.faceStandardMap t x) = extendFaceCoordinates (↑t) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardMap_restrictToFaceSimplex (K : IntrinsicTwoComplex) (t : K.Face) (x : K.realization) (hx : ∀ v ∉ ↑t, ↑x v = 0) : K.faceStandardMap t (K.restrictToFaceSimplex t x hx) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_faceStandardMap (K : IntrinsicTwoComplex) (t : K.Face) : Continuous (K.faceStandardMap t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.toLocallyFiniteTriangleComplex (K : IntrinsicTwoComplex) {S : Type u_1} [TopologicalSpace S] (hused : ∀ (v : K.Vertex), ∃ t ∈ K.faces, v ∈ t) (e : K.realization → S) (he : Topology.IsEmbedding e) : LocallyFiniteTriangleComplex S

Regard a finite intrinsic complex with no unused vertices as a locally finite ambient triangle complex.

Equations

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