Finite simplicial complexes in the plane

The shared geometric foundation for the Moise route (Moise, Geometric Topology in Dimensions 2 and 3, Ch. 0 and Ch. 7 conventions): finite complexes of genuine affine simplexes in the Euclidean plane.

The support of a PlaneComplex is defined as the union of the convex hulls of its faces, vertex positions are actual points, faces are affinely independent, and distinct faces meet in the hull of their shared vertex set. None of these fields is satisfiable by bookkeeping alone: face_inter is a genuine geometric constraint (it fails, for example, for two triangles that overlap in an open region).

IsAffineOn/IsPLOn give the honest piecewise-linear predicates: a map is PL on a complex when it is affine on every face of some subdivision. A generic continuous map is not PL on any complex with a 2-face, in contrast to the vacuous IsPLOnSimplexes this replaces.

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMemDecidablePred {α : Type u_1} [DecidableEq α] (v : α) : DecidablePred fun (s : Finset α) => v ∈ s

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.finsetMemDecidablePred v s = Finset.decidableMem v s

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane : Type

The Euclidean plane used throughout the Moise route.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane = EuclideanSpace ℝ (Fin 2)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle (C : Set Plane) : Prop

A closed triangle in the plane: the convex hull of three affinely independent points.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle C = ∃ (p : Fin 3 → LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane), AffineIndependent ℝ p ∧ C = (convexHull ℝ) (Set.range p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.plane_ext {p q : Plane} (h0 : p.ofLp 0 = q.ofLp 0) (h1 : p.ofLp 1 = q.ofLp 1) : p = q

Two plane points with equal coordinates are equal.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineIndependent_finset_coe {ι : Type u_1} {f : ι → Plane} (hf : AffineIndependent ℝ f) {S : Finset Plane} (hS : ∀ a ∈ S, a ∈ Set.range f) : AffineIndependent ℝ Subtype.val

Affine independence transports to the inclusion of a finite set of points contained in the range of the independent family.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineIndependent_finset_of_card_le_two (A : Finset Plane) (hcard : A.card ≤ 2) : AffineIndependent ℝ Subtype.val

Every finite set of at most two distinct plane points is affinely independent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.segment_inter_segment_of_affineIndependent {x y z : Plane} (h : AffineIndependent ℝ ![x, y, z]) : segment ℝ x y ∩ segment ℝ y z = {y}

Adjacent edges of an affinely independent triple meet exactly in the shared vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_mem_openSegment_inter_ball {a b : Plane} (hab : a ≠ b) {r : ℝ} (hr : 0 < r) : ∃ x ∈ openSegment ℝ a b, x ∈ Metric.ball a r

Every positive ball about one endpoint of a nondegenerate segment contains a relative interior point of that segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.endpoint_not_mem_openSegment_of_mem_segment {a b x y : Plane} (hab : a ≠ b) (hxy : x ≠ y) (hx : x ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) : a ∉ openSegment ℝ x y

An endpoint of a nondegenerate segment cannot lie strictly between two distinct points of that segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.segment_subset_of_midpoint_mem_openSegment {P Q A B : Plane} (hPQ : P ≠ Q) (hAline : A ∈ line[ℝ, P, Q]) (hBline : B ∈ line[ℝ, P, Q]) (hmid : (AffineMap.lineMap P Q) (1 / 2) ∈ openSegment ℝ A B) (hAoutside : A ∉ openSegment ℝ P Q) (hBoutside : B ∉ openSegment ℝ P Q) : segment ℝ P Q ⊆ segment ℝ A B

If two collinear points bracket the midpoint of a segment and neither lies in its relative interior, then they bracket the whole segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.endpoint_secondCoords_eq_zero_of_two_axis_points {a b x y : Plane} : a ≠ b → ∀ (hxy : x ≠ y) (hx : x ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) (hx0 : x.ofLp 1 = 0) (hy0 : y.ofLp 1 = 0), a.ofLp 1 = 0 ∧ b.ofLp 1 = 0

If a nondegenerate segment contains two distinct points on the horizontal axis, then both endpoints lie on that axis.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex : Type 1

A finite simplicial complex of affine simplexes in the plane: finitely many vertices at genuine positions, faces of at most three affinely independent vertices, closed under nonempty subsets, with any two face carriers meeting exactly in the carrier of their shared vertex set.

• Vertex : Type

  The (finite) vertex type.

• vertexFintype : Fintype self.Vertex

  The vertex type is finite.

• vertexDecidableEq : DecidableEq self.Vertex

  Vertices have decidable equality.

• position : self.Vertex → Plane

  The position of each vertex in the plane.

• position_injective : Function.Injective self.position

  Distinct vertices sit at distinct points.

• simplexes : Finset (Finset self.Vertex)

  The faces (simplexes) of the complex, as vertex sets.

• nonempty_of_mem (s : Finset self.Vertex) : s ∈ self.simplexes → s.Nonempty

  Faces are nonempty.

• card_le_three (s : Finset self.Vertex) : s ∈ self.simplexes → s.card ≤ 3

  Faces have at most three vertices: the complex is at most two-dimensional.

• down_closed (s : Finset self.Vertex) : s ∈ self.simplexes → ∀ s' ⊆ s, s'.Nonempty → s' ∈ self.simplexes

  Faces are closed under passing to nonempty subsets.

• affineIndependent (s : Finset self.Vertex) : s ∈ self.simplexes → AffineIndependent ℝ fun (v : ↥s) => self.position ↑v

  The vertices of each face are affinely independent, so its carrier is a genuine geometric simplex of dimension card - 1.

• face_inter (s : Finset self.Vertex) : s ∈ self.simplexes → ∀ t ∈ self.simplexes, (convexHull ℝ) (self.position '' ↑s) ∩ (convexHull ℝ) (self.position '' ↑t) = (convexHull ℝ) (self.position '' ↑(s ∩ t))

  Face carriers intersect exactly in the carrier of their shared vertices. This is the face-to-face condition that makes the complex simplicial rather than an arbitrary union.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh : Type 1

A finite mesh specified only by its maximal triangles. This is the convenient construction interface for line subdivision: all vertices, edges, and singleton faces are generated by TriangleMesh.toPlaneComplex.

• Vertex : Type

  The Vertex declaration.

• vertexFintype : Fintype self.Vertex
• vertexDecidableEq : DecidableEq self.Vertex
• position : self.Vertex → Plane

  The position declaration.

• position_injective : Function.Injective self.position
• triangles : Finset (Finset self.Vertex)

  The triangles declaration.

• card_triangle (t : Finset self.Vertex) : t ∈ self.triangles → t.card = 3
• affineIndependent_triangle (t : Finset self.Vertex) : t ∈ self.triangles → AffineIndependent ℝ fun (v : ↥t) => self.position ↑v
• triangle_inter (s : Finset self.Vertex) : s ∈ self.triangles → ∀ t ∈ self.triangles, (convexHull ℝ) (self.position '' ↑s) ∩ (convexHull ℝ) (self.position '' ↑t) = (convexHull ℝ) (self.position '' ↑(s ∩ t))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.single (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : TriangleMesh

The mesh consisting of one geometric triangle.

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mapAffineEquiv (M : TriangleMesh) (e : Plane ≃ᵃ[ℝ] Plane) : TriangleMesh

Transport a triangle mesh by an affine equivalence of the plane.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.reposition (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : TriangleMesh

Reposition the vertices of a triangle mesh while retaining its abstract triangles. The caller supplies the geometric nondegeneracy and face-to-face proofs for the new positions.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.reposition_triangles (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : (M.reposition position' hposition_injective haffineIndependent htriangle_inter).triangles = M.triangles

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

Delete one maximal triangle from a mesh. Vertices no longer used by any triangle are retained; this keeps the vertex type and geometric positions definitionally unchanged.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.eraseTriangle_triangles (M : TriangleMesh) (t : Finset M.Vertex) : (M.eraseTriangle t).triangles = M.triangles.erase t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_eraseTriangle_triangles (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : (M.eraseTriangle t).triangles.card + 1 = M.triangles.card

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.reindex (M : TriangleMesh) {V' : Type} [Fintype V'] [DecidableEq V'] (position' : V' → Plane) (hposition_injective : Function.Injective position') (e : M.Vertex ↪ V') (hposition : ∀ (v : M.Vertex), position' (e v) = M.position v) : TriangleMesh

Reindex a triangle mesh inside a larger finite vertex type without changing any geometric positions. Extra vertices of the target type may be unused.

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.restrictTriangles (M : TriangleMesh) (p : Finset M.Vertex → Prop) [DecidablePred p] : TriangleMesh

Keep a selected collection of maximal triangles. Unused vertices remain in the ambient finite vertex type; they do not contribute faces or support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_restrictTriangles_triangles (M : TriangleMesh) (p : Finset M.Vertex → Prop) [DecidablePred p] {t : Finset M.Vertex} : t ∈ (M.restrictTriangles p).triangles ↔ t ∈ M.triangles ∧ p t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mapAffineEquiv_triangles (M : TriangleMesh) (e : Plane ≃ᵃ[ℝ] Plane) : (M.mapAffineEquiv e).triangles = M.triangles

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

The nonempty subfaces of all maximal triangles in a triangle mesh.

Equations

• M.faces = M.triangles.biUnion fun (t : Finset M.Vertex) => {x ∈ t.powerset | x.Nonempty}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_faces_iff (M : TriangleMesh) {s : Finset M.Vertex} : s ∈ M.faces ↔ s.Nonempty ∧ ∃ t ∈ M.triangles, s ⊆ t

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.toPlaneComplex (M : TriangleMesh) : PlaneComplex

Every finite triangle mesh determines a finite plane complex.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cellCarrier (K : PlaneComplex) (s : Finset K.Vertex) : Set Plane

The carrier of a face: the convex hull of its vertex positions.

Equations

• K.cellCarrier s = (convexHull ℝ) (K.position '' ↑s)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.support (K : PlaneComplex) : Set Plane

The support of the complex: the union of its face carriers.

Equations

• K.support = ⋃ s ∈ K.simplexes, K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cellCarrier_subset_support (K : PlaneComplex) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : K.cellCarrier s ⊆ K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.isCompact_cellCarrier (K : PlaneComplex) (s : Finset K.Vertex) : IsCompact (K.cellCarrier s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.isCompact_support (K : PlaneComplex) : IsCompact K.support

The support of a finite plane complex is compact.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapAffineEquiv (K : PlaneComplex) (e : Plane ≃ᵃ[ℝ] Plane) : PlaneComplex

Transport a finite plane complex through an affine equivalence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapAffineEquiv_simplexes (K : PlaneComplex) (e : Plane ≃ᵃ[ℝ] Plane) : (K.mapAffineEquiv e).simplexes = K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapAffineEquiv_cellCarrier (K : PlaneComplex) (e : Plane ≃ᵃ[ℝ] Plane) (s : Finset K.Vertex) : (K.mapAffineEquiv e).cellCarrier s = ⇑e '' K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapAffineEquiv_support (K : PlaneComplex) (e : Plane ≃ᵃ[ℝ] Plane) : (K.mapAffineEquiv e).support = ⇑e '' K.support

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cells (K : PlaneComplex) : Finset (Finset K.Vertex)

The two-dimensional faces.

Equations

• K.cells = {s ∈ K.simplexes | s.card = 3}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edges (K : PlaneComplex) : Finset (Finset K.Vertex)

The edges (one-dimensional faces).

Equations

• K.edges = {s ∈ K.simplexes | s.card = 2}

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton (K : PlaneComplex) : PlaneComplex

The subcomplex consisting of the vertices and edges of K.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_oneSkeleton_simplexes (K : PlaneComplex) {s : Finset K.Vertex} : s ∈ K.oneSkeleton.simplexes ↔ s ∈ K.simplexes ∧ s.card ≤ 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton_position (K : PlaneComplex) : K.oneSkeleton.position = K.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton_cellCarrier (K : PlaneComplex) (s : Finset K.Vertex) : K.oneSkeleton.cellCarrier s = K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton_support_subset (K : PlaneComplex) : K.oneSkeleton.support ⊆ K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton_support_eq (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : K.oneSkeleton.support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.oneSkeleton_isGraph (K : PlaneComplex) (s : Finset K.oneSkeleton.Vertex) : s ∈ K.oneSkeleton.simplexes → s.card ≤ 2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.subordinateTo (L K : PlaneComplex) : PlaneComplex

Keep the faces of L which lie in a face of K. This is the standard way to turn an ambient line arrangement into a subdivision subordinate to a pre-existing complex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_subordinateTo_simplexes_iff (L K : PlaneComplex) {s : Finset L.Vertex} : s ∈ (L.subordinateTo K).simplexes ↔ s ∈ L.simplexes ∧ ∃ t ∈ K.simplexes, L.cellCarrier s ⊆ K.cellCarrier t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.subordinateTo_position (L K : PlaneComplex) : (L.subordinateTo K).position = L.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.subordinateTo_cellCarrier (L K : PlaneComplex) (s : Finset L.Vertex) : (L.subordinateTo K).cellCarrier s = L.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.subordinateTo_support_subset (L K : PlaneComplex) : (L.subordinateTo K).support ⊆ K.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictToSet (K : PlaneComplex) (A : Set Plane) : PlaneComplex

Keep precisely the faces whose carriers lie in a prescribed geometric set.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_restrictToSet_simplexes_iff (K : PlaneComplex) (A : Set Plane) {s : Finset K.Vertex} : s ∈ (K.restrictToSet A).simplexes ↔ s ∈ K.simplexes ∧ K.cellCarrier s ⊆ A

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictToSet_cellCarrier (K : PlaneComplex) (A : Set Plane) (s : Finset K.Vertex) : (K.restrictToSet A).cellCarrier s = K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictToSet_support_subset (K : PlaneComplex) (A : Set Plane) : (K.restrictToSet A).support ⊆ A

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsPure2 (K : PlaneComplex) : Prop

A complex is purely two-dimensional when every face lies in a two-dimensional one.

Equations

• K.IsPure2 = ∀ s ∈ K.simplexes, ∃ t ∈ K.simplexes, s ⊆ t ∧ t.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.toPlaneComplex_support (M : TriangleMesh) : M.toPlaneComplex.support = ⋃ t ∈ M.triangles, (convexHull ℝ) (M.position '' ↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.eraseTriangle_support_subset (M : TriangleMesh) (t : Finset M.Vertex) : (M.eraseTriangle t).toPlaneComplex.support ⊆ M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.support_eq_eraseTriangle_union_triangleCarrier (M : TriangleMesh) {t : Finset M.Vertex} (ht : t ∈ M.triangles) : M.toPlaneComplex.support = (M.eraseTriangle t).toPlaneComplex.support ∪ (convexHull ℝ) (M.position '' ↑t)

The support of a mesh is the union of one maximal triangle and the support left after deleting it.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.single_support (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : (single p hp).toPlaneComplex.support = (convexHull ℝ) (Set.range p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.toPlaneComplex_isPure2 (M : TriangleMesh) : M.toPlaneComplex.IsPure2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.toPlaneComplex_cells (M : TriangleMesh) : M.toPlaneComplex.cells = M.triangles

The two-dimensional cells generated by a triangle mesh are exactly its listed maximal triangles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mapAffineEquiv_support (M : TriangleMesh) (e : Plane ≃ᵃ[ℝ] Plane) : (M.mapAffineEquiv e).toPlaneComplex.support = ⇑e '' M.toPlaneComplex.support

Affine transport carries the support of a triangle mesh to the affine image of its original support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.reindex_support (M : TriangleMesh) {V' : Type} [Fintype V'] [DecidableEq V'] (position' : V' → Plane) (hposition_injective : Function.Injective position') (e : M.Vertex ↪ V') (hposition : ∀ (v : M.Vertex), position' (e v) = M.position v) : (M.reindex position' hposition_injective e hposition).toPlaneComplex.support = M.toPlaneComplex.support

Reindexing without changing positions preserves support.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.Subdivides (K' K : PlaneComplex) : Prop

K' subdivides K: same support, and every face carrier of K' lies inside some face carrier of K.

Equations

• K'.Subdivides K = (K'.support = K.support ∧ ∀ s' ∈ K'.simplexes, ∃ s ∈ K.simplexes, K'.cellCarrier s' ⊆ K.cellCarrier s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.Subdivides.refl (K : PlaneComplex) : K.Subdivides K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.Subdivides.trans {K₂ K₁ K₀ : PlaneComplex} (h₂₁ : K₂.Subdivides K₁) (h₁₀ : K₁.Subdivides K₀) : K₂.Subdivides K₀

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.Subdivides.mapAffineEquiv {K' K : PlaneComplex} (h : K'.Subdivides K) (e : Plane ≃ᵃ[ℝ] Plane) : (K'.mapAffineEquiv e).Subdivides (K.mapAffineEquiv e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.subordinateTo_subdivides (L K : PlaneComplex) (hsupport : (L.subordinateTo K).support = K.support) : (L.subordinateTo K).Subdivides K

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn (f : Plane → Plane) (A : Set Plane) : Prop

f agrees with an affine map on A.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn (K : PlaneComplex) (f : Plane → Plane) : Prop

f is piecewise linear on the complex K: affine on every face of some subdivision.

This is the honest PL predicate: a map that is not affine on any neighborhood of a point interior to a 2-cell of K cannot satisfy it, in contrast to the vacuous IsPLOnSimplexes of the retiring PL.lean layer.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLEmbeddingOn (K : PlaneComplex) (f : Plane → Plane) : Prop

f is a PL embedding of the support of K: piecewise linear and injective on the support.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLEmbeddingOn K f = (LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn K f ∧ Set.InjOn f K.support)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOnSet (A : Set Plane) (f : Plane → Plane) : Prop

A function is PL on a geometric set when the set is the support of a finite plane complex on which the function is PL.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn.mono {f : Plane → Plane} {A B : Set Plane} (hf : IsAffineOn f A) (hBA : B ⊆ A) : IsAffineOn f B

Restrict an affine-on-set witness to a smaller set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn.comp {f g : Plane → Plane} {A B : Set Plane} (hg : IsAffineOn g B) (hf : IsAffineOn f A) (hmap : Set.MapsTo f A B) : IsAffineOn (g ∘ f) A

Composition of affine-on-set maps is affine when the first map carries the source set into the set on which the second map is affine.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn.continuousOn {f : Plane → Plane} {A : Set Plane} (hf : IsAffineOn f A) : ContinuousOn f A

A function agreeing with an affine map on a set is continuous there.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn.image_segment {f : Plane → Plane} {A : Set Plane} (hf : IsAffineOn f A) {x y : Plane} (hsegment : segment ℝ x y ⊆ A) : f '' segment ℝ x y = segment ℝ (f x) (f y)

An affine-on-set map sends every segment contained in the set to the segment between the endpoint images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsAffineOn.image_convexHull {f : Plane → Plane} {A : Set Plane} (hf : IsAffineOn f ((convexHull ℝ) A)) : (convexHull ℝ) (f '' A) = f '' (convexHull ℝ) A

An affine-on-hull map carries a finite convex hull to the convex hull of the images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn.of_affineOn_support {K : PlaneComplex} {f : Plane → Plane} (hf : IsAffineOn f K.support) : IsPLOn K f

A map affine on the support is PL without further subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn.of_subdivision {K' K : PlaneComplex} {f : Plane → Plane} (hsubdivision : K'.Subdivides K) (hf : IsPLOn K' f) : IsPLOn K f

A PL witness on a subdivision is also a PL witness on the original complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn.continuousOn {K : PlaneComplex} {f : Plane → Plane} (hf : IsPLOn K f) : ContinuousOn f K.support

A PL map is continuous on the support of its complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPLOn.affineConjugate {K : PlaneComplex} {f : Plane → Plane} (hf : IsPLOn K f) (source target : Plane ≃ᵃ[ℝ] Plane) : IsPLOn (K.mapAffineEquiv source) fun (x : Plane) => target (f (source.symm x))

PL maps remain PL after affine changes of coordinates in source and target.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_simplexes_of_mem_cells (K : PlaneComplex) {t : Finset K.Vertex} (ht : t ∈ K.cells) : t ∈ K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.card_of_mem_cells (K : PlaneComplex) {t : Finset K.Vertex} (ht : t ∈ K.cells) : t.card = 3

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEval (K : PlaneComplex) (x : K.Vertex → ℝ) : Plane

Barycentric evaluation: the point of the plane with the given barycentric weights.

Equations

• K.baryEval x = ∑ v : K.Vertex, x v • K.position v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.continuous_baryEval (K : PlaneComplex) : Continuous fun (x : K.Vertex → ℝ) => K.baryEval x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEval_eq_sum_of_support (K : PlaneComplex) {x : K.Vertex → ℝ} {t : Finset K.Vertex} (hsupp : ∀ v ∉ t, x v = 0) : K.baryEval x = ∑ v ∈ t, x v • K.position v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sum_eq_sum_of_support (K : PlaneComplex) {x : K.Vertex → ℝ} {t : Finset K.Vertex} (hsupp : ∀ v ∉ t, x v = 0) : ∑ v : K.Vertex, x v = ∑ v ∈ t, x v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEval_mem_cellCarrier (K : PlaneComplex) {x : K.Vertex → ℝ} {t : Finset K.Vertex} (hsupp : ∀ v ∉ t, x v = 0) (h0 : ∀ (v : K.Vertex), 0 ≤ x v) (h1 : ∑ v : K.Vertex, x v = 1) : K.baryEval x ∈ K.cellCarrier t

Barycentric evaluation of weights supported on a face lands in that face's carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_weights_of_mem_cellCarrier (K : PlaneComplex) {p : Plane} {t : Finset K.Vertex} (hp : p ∈ K.cellCarrier t) : ∃ (x : K.Vertex → ℝ), (∀ v ∉ t, x v = 0) ∧ (∀ (v : K.Vertex), 0 ≤ x v) ∧ ∑ v : K.Vertex, x v = 1 ∧ K.baryEval x = p

Every point of a face carrier has barycentric weights supported on that face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEval_injOn_face (K : PlaneComplex) {t : Finset K.Vertex} (ht : t ∈ K.simplexes) {x y : K.Vertex → ℝ} (hx : ∀ v ∉ t, x v = 0) (hy : ∀ v ∉ t, y v = 0) (hx1 : ∑ v : K.Vertex, x v = 1) (hy1 : ∑ v : K.Vertex, y v = 1) (heq : K.baryEval x = K.baryEval y) : x = y

Barycentric weights on an affinely independent face are unique.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorph (K : PlaneComplex) (hpure : K.IsPure2) : ↑(GeometricRealization K.Vertex K.cells) ≃ₜ ↑K.support

The canonical barycentric homeomorphism from the abstract realization of a pure plane complex to its geometric support.

Equations

• K.realizationHomeomorph hpure = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorph_apply (K : PlaneComplex) (hpure : K.IsPure2) (x : ↑(GeometricRealization K.Vertex K.cells)) : ↑((K.realizationHomeomorph hpure) x) = K.baryEval ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toGeometricTriangulation (K : PlaneComplex) (hpure : K.IsPure2) : Nonempty (GeometricTriangulation ↑K.support)

Realization bridge (elementary): a purely two-dimensional plane complex induces a geometric triangulation of its support, by barycentric coordinates in the face containing each point. Injectivity is the uniqueness of barycentric coordinates on each affinely independent face, glued across faces by the face-to-face intersection condition.