Polygonal arcs from broken lines

This is the finite-arrangement layer needed between Moise Chapter 6, Theorems 1 and 2. The connectivity theorem produces an arbitrary finite chain of segments. Subdividing a large triangle by the supporting lines of those segments, and by two coordinate lines through every chain vertex, turns all crossings and all chain vertices into vertices of one finite triangle mesh. A simple graph path in the resulting one-skeleton is then a loop-free polygonal arc.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData (U : Set Plane) : Type

Concrete data carried by a broken-line witness.

• n : ℕ

  The n declaration.

• vertex : Fin (self.n + 1) → Plane

  The vertex declaration.

• segment_subset (i : Fin self.n) : segment ℝ (self.vertex i.castSucc) (self.vertex i.succ) ⊆ U

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.start {U : Set Plane} (B : BrokenLineData U) : Plane

The start declaration.

Equations

• B.start = B.vertex 0

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.finish {U : Set Plane} (B : BrokenLineData U) : Plane

The finish declaration.

Equations

• B.finish = B.vertex (Fin.last B.n)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyChain {I : Type u_1} [Fintype I] (left right : I → Plane) : BrokenLineData Set.univ

An auxiliary broken line listing an arbitrary finite family of segments. The prescribed segments occur at the even indices; the odd indices are disposable connectors. This is the common-arrangement input used when several independently constructed polygonal arcs must be viewed in one finite plane complex.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyIndex {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : Fin (segmentFamilyChain left right).n

The even index carrying the segment labelled by i.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyIndex left right i = ⟨2 * ↑((Fintype.equivFin I) i), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyChain_vertex_even {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyChain left right).vertex ⟨2 * ↑((Fintype.equivFin I) i), ⋯⟩ = left i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyChain_vertex_odd {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyChain left right).vertex ⟨2 * ↑((Fintype.equivFin I) i) + 1, ⋯⟩ = right i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyIndex_castSucc {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyIndex left right i).castSucc = ⟨2 * ↑((Fintype.equivFin I) i), ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyIndex_succ {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyIndex left right i).succ = ⟨2 * ↑((Fintype.equivFin I) i) + 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamilyChain_segment {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : segment ℝ ((segmentFamilyChain left right).vertex (segmentFamilyIndex left right i).castSucc) ((segmentFamilyChain left right).vertex (segmentFamilyIndex left right i).succ) = segment ℝ (left i) (right i)

The segment at the distinguished even index is exactly the requested family member.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_data_of_joined {U : Set Plane} {a b : Plane} (h : JoinedByBrokenLine U a b) : ∃ (B : BrokenLineData U), B.start = a ∧ B.finish = b

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLine (a b : Plane) : Plane →ᵃ[ℝ] ℝ

The affine functional whose zero set contains the line through a and b.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLine_apply_left (a b : Plane) : (segmentLine a b) a = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLine_apply_right (a b : Plane) : (segmentLine a b) b = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLine_eq_zero_of_mem_segment (a b : Plane) {x : Plane} (hx : x ∈ segment ℝ a b) : (segmentLine a b) x = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.mem_segment_of_segmentLine_eq_zero {a b x : Plane} (hab : a ≠ b) (hline : (segmentLine a b) x = 0) (hx0 : x.ofLp 0 ∈ Set.uIcc (a.ofLp 0) (b.ofLp 0)) (hx1 : x.ofLp 1 ∈ Set.uIcc (a.ofLp 1) (b.ofLp 1)) : x ∈ segment ℝ a b

A point on the supporting line of a nondegenerate segment belongs to the segment exactly when its coordinates lie between the endpoint coordinates. Both coordinate hypotheses make the statement symmetric and avoid selecting a preferred nonconstant coordinate in its interface.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.verticalLine (p : Plane) : Plane →ᵃ[ℝ] ℝ

The verticalLine declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.horizontalLine (p : Plane) : Plane →ᵃ[ℝ] ℝ

The horizontalLine declaration.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.verticalLine_apply_self (p : Plane) : (verticalLine p) p = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.horizontalLine_apply_self (p : Plane) : (horizontalLine p) p = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLines {U : Set Plane} (B : BrokenLineData U) : List (Plane →ᵃ[ℝ] ℝ)

Supporting lines of the chain segments.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.vertexLines {U : Set Plane} (B : BrokenLineData U) : List (Plane →ᵃ[ℝ] ℝ)

Coordinate lines force every chain vertex to become an arrangement vertex, including at a collinear turn or a degenerate segment.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementLines {U : Set Plane} (B : BrokenLineData U) : List (Plane →ᵃ[ℝ] ℝ)

The arrangementLines declaration.

Equations

• B.arrangementLines = B.segmentLines ++ B.vertexLines

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.enclosingRadius {U : Set Plane} (B : BrokenLineData U) : ℝ

A positive radius containing every chain vertex.

Equations

• B.enclosingRadius = 1 + ∑ i : Fin (B.n + 1), ‖B.vertex i‖

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.enclosingRadius_pos {U : Set Plane} (B : BrokenLineData U) : 0 < B.enclosingRadius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.vertex_mem_enclosingBall {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : B.vertex i ∈ Metric.closedBall 0 B.enclosingRadius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segment_subset_enclosingBall {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : segment ℝ (B.vertex i.castSucc) (B.vertex i.succ) ⊆ Metric.closedBall 0 B.enclosingRadius

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.enclosingMesh {U : Set Plane} (B : BrokenLineData U) : TriangleMesh

The enclosingMesh declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementMesh {U : Set Plane} (B : BrokenLineData U) : TriangleMesh

The finite line arrangement resolving every segment crossing and chain vertex.

Equations

• B.arrangementMesh = B.enclosingMesh.refineByLines B.arrangementLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementMesh_support {U : Set Plane} (B : BrokenLineData U) : B.arrangementMesh.toPlaneComplex.support = (convexHull ℝ) (Set.range (PolygonalCircle.enclosingTriangleVertices B.enclosingRadius))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segment_subset_arrangementMesh_support {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : segment ℝ (B.vertex i.castSucc) (B.vertex i.succ) ⊆ B.arrangementMesh.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentLine_mem_arrangementLines {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : segmentLine (B.vertex i.castSucc) (B.vertex i.succ) ∈ B.arrangementLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.verticalLine_mem_arrangementLines {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : verticalLine (B.vertex i) ∈ B.arrangementLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.horizontalLine_mem_arrangementLines {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : horizontalLine (B.vertex i) ∈ B.arrangementLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementMesh_monochromatic_segmentLine {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : B.arrangementMesh.IsMonochromatic (segmentLine (B.vertex i.castSucc) (B.vertex i.succ))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementMesh_monochromatic_verticalLine {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : B.arrangementMesh.IsMonochromatic (verticalLine (B.vertex i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementMesh_monochromatic_horizontalLine {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : B.arrangementMesh.IsMonochromatic (horizontalLine (B.vertex i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_zero_face_of_mem_support (M : TriangleMesh) {f : Plane →ᵃ[ℝ] ℝ} (hmono : M.IsMonochromatic f) {x : Plane} (hx : x ∈ M.toPlaneComplex.support) (hfx : f x = 0) : ∃ s ∈ M.toPlaneComplex.simplexes, x ∈ M.toPlaneComplex.cellCarrier s ∧ ∀ v ∈ s, f (M.position v) = 0

In a triangulation monochromatic for an affine functional, every point of its zero set lies in a face all of whose vertices are zero.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_vertex_position_eq_of_monochromatic_coordinates (M : TriangleMesh) (p : Plane) (hp : p ∈ M.toPlaneComplex.support) (hx : M.IsMonochromatic (BrokenLineData.verticalLine p)) (hy : M.IsMonochromatic (BrokenLineData.horizontalLine p)) : ∃ (v : M.Vertex), M.toPlaneComplex.position v = p ∧ {v} ∈ M.toPlaneComplex.simplexes

Two monochromatic coordinate lines through a supported point force that point to occur as an actual mesh vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.nonneg_on_face_of_monochromatic_of_pos (M : TriangleMesh) {f : Plane →ᵃ[ℝ] ℝ} (hmono : M.IsMonochromatic f) {s : Finset M.Vertex} (hs : s ∈ M.toPlaneComplex.simplexes) {x : Plane} (hxs : x ∈ M.toPlaneComplex.cellCarrier s) (hfx : 0 < f x) (v : M.Vertex) : v ∈ s → 0 ≤ f (M.position v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.nonpos_on_face_of_monochromatic_of_neg (M : TriangleMesh) {f : Plane →ᵃ[ℝ] ℝ} (hmono : M.IsMonochromatic f) {s : Finset M.Vertex} (hs : s ∈ M.toPlaneComplex.simplexes) {x : Plane} (hxs : x ∈ M.toPlaneComplex.cellCarrier s) (hfx : f x < 0) (v : M.Vertex) : v ∈ s → f (M.position v) ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.card_le_two_of_vertices_mem_segment (K : PlaneComplex) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) {a b : Plane} (hseg : ∀ v ∈ s, K.position v ∈ segment ℝ a b) : s.card ≤ 2

An affine-independent face whose vertices lie on one segment has at most two vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_vertex_pair_segment_of_mem_cellCarrier (K : PlaneComplex) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) (hcard : s.card ≤ 2) {x : Plane} (hx : x ∈ K.cellCarrier s) : ∃ (v : K.Vertex) (w : K.Vertex), v ∈ s ∧ w ∈ s ∧ x ∈ segment ℝ (K.position v) (K.position w)

A point in a nonempty face of cardinality at most two lies on a segment joining two of that face's vertices (the two vertices may coincide for a zero-face).

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexGraph (K : PlaneComplex) : SimpleGraph K.Vertex

The graph formed by the one-dimensional faces of a plane complex.

Equations

• K.vertexGraph = { Adj := fun (v w : K.Vertex) => v ≠ w ∧ {v, w} ∈ K.simplexes, symm := ⋯, loopless := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexGraph_adj_iff (K : PlaneComplex) {v w : K.Vertex} : K.vertexGraph.Adj v w ↔ v ≠ w ∧ {v, w} ∈ K.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.position_mem_support_of_mem_walk (K : PlaneComplex) {u v w : K.Vertex} (p : K.vertexGraph.Walk u v) (hv : {v} ∈ K.simplexes) (hw : w ∈ p.support) : K.position w ∈ K.support

Every vertex visited by a one-skeleton walk is geometrically supported, provided the final vertex is an actual zero-face. All earlier vertices occur in an edge of the walk.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inducedBy (K : PlaneComplex) (p : K.Vertex → Prop) : PlaneComplex

The induced subcomplex on the vertices satisfying p. Vertices outside p remain in the ambient finite type but occur in no face; PlaneComplex.active can remove them when desired.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inducedBy_position (K : PlaneComplex) (p : K.Vertex → Prop) : (K.inducedBy p).position = K.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inducedBy_cellCarrier (K : PlaneComplex) (p : K.Vertex → Prop) (s : Finset K.Vertex) : (K.inducedBy p).cellCarrier s = K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mem_inducedBy_simplexes_iff (K : PlaneComplex) (p : K.Vertex → Prop) {s : Finset K.Vertex} : s ∈ (K.inducedBy p).simplexes ↔ s ∈ K.simplexes ∧ ∀ v ∈ s, p v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inducedBy_support_subset (K : PlaneComplex) {C : Set Plane} (hC : Convex ℝ C) (p : K.Vertex → Prop) (hp : ∀ (v : K.Vertex), p v → K.position v ∈ C) : (K.inducedBy p).support ⊆ C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inducedBy_support_eq (K : PlaneComplex) {C : Set Plane} (hC : Convex ℝ C) (p : K.Vertex → Prop) (hp : ∀ (v : K.Vertex), p v → K.position v ∈ C) (hcover : ∀ x ∈ C, ∃ s ∈ K.simplexes, x ∈ K.cellCarrier s ∧ ∀ v ∈ s, p v) : (K.inducedBy p).support = C

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictedTo (K : PlaneComplex) (C : Set Plane) : PlaneComplex

The subcomplex consisting of exactly those faces whose whole geometric carrier lies in C. Unlike inducedBy, this is appropriate when C is a nonconvex polygonal set.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictedTo_position (K : PlaneComplex) (C : Set Plane) : (K.restrictedTo C).position = K.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictedTo_cellCarrier (K : PlaneComplex) (C : Set Plane) (s : Finset K.Vertex) : (K.restrictedTo C).cellCarrier s = K.cellCarrier s

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictedTo_support_subset (K : PlaneComplex) (C : Set Plane) : (K.restrictedTo C).support ⊆ C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.restrictedTo_support_eq (K : PlaneComplex) (C : Set Plane) (hcover : ∀ x ∈ C, ∃ s ∈ K.simplexes, x ∈ K.cellCarrier s ∧ K.cellCarrier s ⊆ C) : (K.restrictedTo C).support = C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexGraph_reachable_of_mem_simplex (K : PlaneComplex) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) {v w : K.Vertex} (hv : v ∈ s) (hw : w ∈ s) : K.vertexGraph.Reachable v w

All vertices of one simplex lie in one reachability class of the vertex graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexGraph_reachable_of_isPreconnected (K : PlaneComplex) (hconn : IsPreconnected K.support) {u v : K.Vertex} (hu : {u} ∈ K.simplexes) (hv : {v} ∈ K.simplexes) : K.vertexGraph.Reachable u v

If the support of a finite plane complex is connected, then any two vertices which actually occur as zero-faces are joined by a path in its one-skeleton.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_arrangementVertex_position_eq {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : ∃ (v : B.arrangementMesh.Vertex), B.arrangementMesh.toPlaneComplex.position v = B.vertex i ∧ {v} ∈ B.arrangementMesh.toPlaneComplex.simplexes

Every original chain vertex is a vertex of the line-arrangement mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_face_on_segment {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) {x : Plane} (hx : x ∈ segment ℝ (B.vertex i.castSucc) (B.vertex i.succ)) : ∃ s ∈ B.arrangementMesh.toPlaneComplex.simplexes, x ∈ B.arrangementMesh.toPlaneComplex.cellCarrier s ∧ ∀ v ∈ s, B.arrangementMesh.toPlaneComplex.position v ∈ segment ℝ (B.vertex i.castSucc) (B.vertex i.succ)

Every point of an original nondegenerate chain segment lies in an arrangement face whose vertices all lie on that segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_face_on_segmentFamily {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) {x : Plane} (hx : x ∈ segment ℝ (left i) (right i)) : ∃ s ∈ (segmentFamilyChain left right).arrangementMesh.toPlaneComplex.simplexes, x ∈ (segmentFamilyChain left right).arrangementMesh.toPlaneComplex.cellCarrier s ∧ (segmentFamilyChain left right).arrangementMesh.toPlaneComplex.cellCarrier s ⊆ segment ℝ (left i) (right i)

The common arrangement of a finite segment family resolves each requested member into faces contained in that member. Keeping this theorem abstract in the family index prevents clients with dependent finite index types from unfolding their entire enumeration during kernel checking.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentCarrier {U : Set Plane} (B : BrokenLineData U) : Set Plane

The geometric carrier of all listed segments of a finite broken line. Auxiliary line arrangements may contain many additional faces, so this is the carrier relevant to the polygonal object itself.

Equations

• B.segmentCarrier = ⋃ (i : Fin B.n), segment ℝ (B.vertex i.castSucc) (B.vertex i.succ)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.carrierComplex {U : Set Plane} (B : BrokenLineData U) : PlaneComplex

The line arrangement restricted to the actual segments of a finite broken line. This is a canonical finite plane complex even when the listed segments cross or overlap: the ambient line arrangement has already inserted every required intersection vertex.

Equations

• B.carrierComplex = B.arrangementMesh.toPlaneComplex.restrictToSet B.segmentCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.carrierComplex_support {U : Set Plane} (B : BrokenLineData U) : B.carrierComplex.support = B.segmentCarrier

The canonical complex of a broken line has exactly the union of its listed segments as support.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementVertex {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : B.arrangementMesh.toPlaneComplex.Vertex

A canonical arrangement vertex representing an original chain vertex.

Equations

• B.arrangementVertex i = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementVertex_position {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : B.arrangementMesh.toPlaneComplex.position (B.arrangementVertex i) = B.vertex i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementVertex_face {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.n + 1)) : {B.arrangementVertex i} ∈ B.arrangementMesh.toPlaneComplex.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamily_arrangementVertex_position_left {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyChain left right).arrangementMesh.toPlaneComplex.position ((segmentFamilyChain left right).arrangementVertex (segmentFamilyIndex left right i).castSucc) = left i

The left endpoint of a listed family segment is a canonical vertex of the common arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentFamily_arrangementVertex_position_right {I : Type u_1} [Fintype I] (left right : I → Plane) (i : I) : (segmentFamilyChain left right).arrangementMesh.toPlaneComplex.position ((segmentFamilyChain left right).arrangementVertex (segmentFamilyIndex left right i).succ) = right i

The right endpoint of a listed family segment is a canonical vertex of the common arrangement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentComplex {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : PlaneComplex

The part of the arrangement mesh lying wholly on one original chain segment.

Equations

• B.segmentComplex i = B.arrangementMesh.toPlaneComplex.restrictedTo (segment ℝ (B.vertex i.castSucc) (B.vertex i.succ))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentComplex_support {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : (B.segmentComplex i).support = segment ℝ (B.vertex i.castSucc) (B.vertex i.succ)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementVertex_mem_segmentComplex_left {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : {B.arrangementVertex i.castSucc} ∈ (B.segmentComplex i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.arrangementVertex_mem_segmentComplex_right {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : {B.arrangementVertex i.succ} ∈ (B.segmentComplex i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.reachable_on_segment {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : (B.segmentComplex i).vertexGraph.Reachable (B.arrangementVertex i.castSucc) (B.arrangementVertex i.succ)

The line arrangement turns every original chain segment into a path in a finite one-skeleton.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_path_on_segment {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : Nonempty ((B.segmentComplex i).vertexGraph.Path (B.arrangementVertex i.castSucc) (B.arrangementVertex i.succ))

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.inSetGraph {U : Set Plane} (B : BrokenLineData U) : SimpleGraph B.arrangementMesh.toPlaneComplex.Vertex

Arrangement edges whose geometric segments lie in the prescribed open set.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.inSetGraph_adj_iff {U : Set Plane} (B : BrokenLineData U) {v w : B.arrangementMesh.toPlaneComplex.Vertex} : B.inSetGraph.Adj v w ↔ v ≠ w ∧ {v, w} ∈ B.arrangementMesh.toPlaneComplex.simplexes ∧ B.arrangementMesh.toPlaneComplex.cellCarrier {v, w} ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.inSetGraph_le_arrangementVertexGraph {U : Set Plane} (B : BrokenLineData U) : B.inSetGraph ≤ B.arrangementMesh.toPlaneComplex.vertexGraph

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.segmentVertexGraph_le_inSetGraph {U : Set Plane} (B : BrokenLineData U) (i : Fin B.n) : (B.segmentComplex i).vertexGraph ≤ B.inSetGraph

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_arrangement_path {U : Set Plane} (B : BrokenLineData U) : Nonempty (B.inSetGraph.Path (B.arrangementVertex 0) (B.arrangementVertex (Fin.last B.n)))

Concatenating the segment paths gives a walk through the entire broken line; Mathlib's loop-erasure then produces a path with the same endpoints.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedPath {U : Set Plane} (B : BrokenLineData U) : B.inSetGraph.Path (B.arrangementVertex 0) (B.arrangementVertex (Fin.last B.n))

A canonical loop-free resolution of the broken line.

Equations

• B.resolvedPath = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedWalk {U : Set Plane} (B : BrokenLineData U) : B.inSetGraph.Walk (B.arrangementVertex 0) (B.arrangementVertex (Fin.last B.n))

The resolvedWalk declaration.

Equations

• B.resolvedWalk = ↑B.resolvedPath

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.resolvedWalk.length + 1)) : Plane

Ordered geometric vertices of the resolved polygonal arc.

Equations

• B.resolvedVertex i = B.arrangementMesh.toPlaneComplex.position (B.resolvedWalk.getVert ↑i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex_injective {U : Set Plane} (B : BrokenLineData U) : Function.Injective B.resolvedVertex

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex_start {U : Set Plane} (B : BrokenLineData U) : B.resolvedVertex 0 = B.start

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex_finish {U : Set Plane} (B : BrokenLineData U) : B.resolvedVertex (Fin.last B.resolvedWalk.length) = B.finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedSegment_subset {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ) ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedSegment_eq_cellCarrier {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ) = B.arrangementMesh.toPlaneComplex.cellCarrier {B.resolvedWalk.getVert ↑i, B.resolvedWalk.getVert (↑i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdge_mem_simplexes {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : {B.resolvedWalk.getVert ↑i, B.resolvedWalk.getVert (↑i + 1)} ∈ B.arrangementMesh.toPlaneComplex.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedSegment_inter {U : Set Plane} (B : BrokenLineData U) (i j : Fin B.resolvedWalk.length) : segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ) ∩ segment ℝ (B.resolvedVertex j.castSucc) (B.resolvedVertex j.succ) = B.arrangementMesh.toPlaneComplex.cellCarrier ({B.resolvedWalk.getVert ↑i, B.resolvedWalk.getVert (↑i + 1)} ∩ {B.resolvedWalk.getVert ↑j, B.resolvedWalk.getVert (↑j + 1)})

Exact face-to-face intersection for the ordered segments of the resolved arc.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedCarrier {U : Set Plane} (B : BrokenLineData U) : Set Plane

The geometric carrier of the selected graph path.

Equations

• B.resolvedCarrier = if x : B.resolvedWalk.length = 0 then {B.resolvedVertex 0} else ⋃ (i : Fin B.resolvedWalk.length), segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedCarrier_subset {U : Set Plane} (B : BrokenLineData U) (hstart : B.start ∈ U) : B.resolvedCarrier ⊆ U

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedComplex {U : Set Plane} (B : BrokenLineData U) : PlaneComplex

The parent-arrangement subcomplex consisting of the chosen path edges and their vertices.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedComplex_position {U : Set Plane} (B : BrokenLineData U) : B.resolvedComplex.position = B.arrangementMesh.toPlaneComplex.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedComplex_cellCarrier {U : Set Plane} (B : BrokenLineData U) (s : Finset B.arrangementMesh.toPlaneComplex.Vertex) : B.resolvedComplex.cellCarrier s = B.arrangementMesh.toPlaneComplex.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.mem_resolvedComplex_simplexes_iff {U : Set Plane} (B : BrokenLineData U) {s : Finset B.arrangementMesh.toPlaneComplex.Vertex} : s ∈ B.resolvedComplex.simplexes ↔ s ∈ B.arrangementMesh.toPlaneComplex.simplexes ∧ LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.IsResolvedFace✝ B s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex_face {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.resolvedWalk.length + 1)) : {B.resolvedWalk.getVert ↑i} ∈ B.resolvedComplex.simplexes

Every ordered vertex of the resolved path occurs as a zero-face of the selected complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedVertex_mem_support {U : Set Plane} (B : BrokenLineData U) (i : Fin (B.resolvedWalk.length + 1)) : B.resolvedComplex.position (B.resolvedWalk.getVert ↑i) ∈ B.resolvedComplex.support

Every ordered path vertex lies in the support of the selected complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedComplex_card_le_two {U : Set Plane} (B : BrokenLineData U) {s : Finset B.resolvedComplex.Vertex} (hs : s ∈ B.resolvedComplex.simplexes) : s.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedComplex_support {U : Set Plane} (B : BrokenLineData U) : B.resolvedComplex.support = B.resolvedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeParameter {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : Plane →ᵃ[ℝ] ℝ

Affine coordinate from 0 to 1 along one resolved path edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeParameter_apply_left {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : (B.resolvedEdgeParameter i) (B.resolvedVertex i.castSucc) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeParameter_apply_right {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : (B.resolvedEdgeParameter i) (B.resolvedVertex i.succ) = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeParameter_lineMap {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) (t : ℝ) : (B.resolvedEdgeParameter i) ((AffineMap.lineMap (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) t) = t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeGlobalParameter {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : Plane →ᵃ[ℝ] ℝ

The affine coordinate on edge i, shifted to the interval [i,i+1].

Equations

• B.resolvedEdgeGlobalParameter i = AffineMap.const ℝ LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane ↑↑i + B.resolvedEdgeParameter i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeGlobalParameter_apply_left {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : (B.resolvedEdgeGlobalParameter i) (B.resolvedVertex i.castSucc) = ↑↑i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeGlobalParameter_apply_right {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) : (B.resolvedEdgeGlobalParameter i) (B.resolvedVertex i.succ) = ↑↑i + 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeGlobalParameter_lineMap {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) (t : ℝ) : (B.resolvedEdgeGlobalParameter i) ((AffineMap.lineMap (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) t) = ↑↑i + t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdge_indices_close {U : Set Plane} (B : BrokenLineData U) (i j : Fin B.resolvedWalk.length) (hinter : ({B.resolvedWalk.getVert ↑i, B.resolvedWalk.getVert (↑i + 1)} ∩ {B.resolvedWalk.getVert ↑j, B.resolvedWalk.getVert (↑j + 1)}).Nonempty) : i = j ∨ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedSegment_indices_close {U : Set Plane} (B : BrokenLineData U) (i j : Fin B.resolvedWalk.length) {x : Plane} (hxi : x ∈ segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) (hxj : x ∈ segment ℝ (B.resolvedVertex j.castSucc) (B.resolvedVertex j.succ)) : i = j ∨ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedSegment_inter_of_succ_eq {U : Set Plane} (B : BrokenLineData U) (i j : Fin B.resolvedWalk.length) (hij : ↑i + 1 = ↑j) : segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ) ∩ segment ℝ (B.resolvedVertex j.castSucc) (B.resolvedVertex j.succ) = {B.resolvedVertex i.succ}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedEdgeGlobalParameter_agree {U : Set Plane} (B : BrokenLineData U) (i j : Fin B.resolvedWalk.length) {x : Plane} (hxi : x ∈ segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) (hxj : x ∈ segment ℝ (B.resolvedVertex j.castSucc) (B.resolvedVertex j.succ)) : (B.resolvedEdgeGlobalParameter i) x = (B.resolvedEdgeGlobalParameter j) x

The shifted affine edge parameters agree wherever two selected path edges meet.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter {U : Set Plane} (B : BrokenLineData U) (x : Plane) : ℝ

Piecewise-affine coordinate along the whole resolved arc.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_eq_on_edge {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) {x : Plane} (hx : x ∈ segment ℝ (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) : B.resolvedGlobalParameter x = (B.resolvedEdgeGlobalParameter i) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_lineMap_of_mem {U : Set Plane} (B : BrokenLineData U) (i : Fin B.resolvedWalk.length) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : B.resolvedGlobalParameter ((AffineMap.lineMap (B.resolvedVertex i.castSucc) (B.resolvedVertex i.succ)) t) = ↑↑i + t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_injectiveOn {U : Set Plane} (B : BrokenLineData U) : Set.InjOn B.resolvedGlobalParameter B.resolvedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_image {U : Set Plane} (B : BrokenLineData U) : B.resolvedGlobalParameter '' B.resolvedCarrier = Set.Icc 0 ↑B.resolvedWalk.length

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_start {U : Set Plane} (B : BrokenLineData U) : B.resolvedGlobalParameter (B.resolvedVertex 0) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedGlobalParameter_finish {U : Set Plane} (B : BrokenLineData U) : B.resolvedGlobalParameter (B.resolvedVertex (Fin.last B.resolvedWalk.length)) = ↑B.resolvedWalk.length

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisLinear : ℝ →ₗ[ℝ] Plane

Affine inclusion of the real axis into the plane.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisAffine : ℝ →ᵃ[ℝ] Plane

The realAxisAffine declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisAffine = LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisLinear.toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisAffine_apply (t : ℝ) : realAxisAffine t = planePoint t 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten {U : Set Plane} (B : BrokenLineData U) (x : Plane) : Plane

Piecewise-affine straightening of the selected polygonal arc onto the real axis.

Equations

• B.resolvedStraighten x = LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisAffine (B.resolvedGlobalParameter x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten_start {U : Set Plane} (B : BrokenLineData U) : B.resolvedStraighten (B.resolvedVertex 0) = planePoint 0 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten_finish {U : Set Plane} (B : BrokenLineData U) : B.resolvedStraighten (B.resolvedVertex (Fin.last B.resolvedWalk.length)) = planePoint (↑B.resolvedWalk.length) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten_injectiveOn {U : Set Plane} (B : BrokenLineData U) : Set.InjOn B.resolvedStraighten B.resolvedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten_image {U : Set Plane} (B : BrokenLineData U) : B.resolvedStraighten '' B.resolvedCarrier = segment ℝ (planePoint 0 0) (planePoint (↑B.resolvedWalk.length) 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedStraighten_affineOn_faces {U : Set Plane} (B : BrokenLineData U) (s : Finset B.resolvedComplex.Vertex) : s ∈ B.resolvedComplex.simplexes → IsAffineOn B.resolvedStraighten (B.resolvedComplex.cellCarrier s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedBrokenLine {U : Set Plane} (B : BrokenLineData U) : BrokenLineData U

The ordered broken-line data underlying the canonical simple graph path.

Equations

• B.resolvedBrokenLine = { n := B.resolvedWalk.length, vertex := B.resolvedVertex, segment_subset := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedBrokenLine_start {U : Set Plane} (B : BrokenLineData U) : B.resolvedBrokenLine.start = B.start

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedBrokenLine_finish {U : Set Plane} (B : BrokenLineData U) : B.resolvedBrokenLine.finish = B.finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.resolvedBrokenLine_vertex_injective {U : Set Plane} (B : BrokenLineData U) : Function.Injective B.resolvedBrokenLine.vertex

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.exists_polygonalArc {U : Set Plane} {a b : Plane} (h : JoinedByBrokenLine U a b) : ∃ (B : BrokenLineData U), B.start = a ∧ B.finish = b ∧ Nonempty (B.inSetGraph.Path (B.arrangementVertex 0) (B.arrangementVertex (Fin.last B.n)))

A weak broken line can be resolved into a loop-free path in a finite straight-line graph, with every graph edge contained in the same set. This is the precise polygonal-arc form of Moise Chapter 6, Theorem 1 used by the graph approximation argument.