Finite PL models for locally finite graph replacements

Each edge of the locally finite replacement graph is still a finite polygonal arc. This file marks its two last-exit parameters, restricts the finite source model to the intervening arc, and adds the two radial spokes. The resulting finite plane complex has exactly the complete replacement edge as support. It is the edge-level input for assembling polygonal face boundaries in a common arrangement.

Piecewise-affine formulas on the canonical edge parameter

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CentralPolygonalArc.completePath_eq_left {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (r : ↑(Set.Icc 0 1)) (hr : ↑r ≤ 1 / 2) : A.completePath r = (AffineMap.lineMap (G.vertexImage (K.edgeFirst e)) A.leftEndpoint) (2 * ↑r)

On the first piece, the complete replacement path is the affine first spoke.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CentralPolygonalArc.completePath_eq_middle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (r : ↑(Set.Icc 0 1)) (hr0 : 1 / 2 ≤ ↑r) (hr1 : ↑r ≤ 3 / 4) : A.completePath r = A.parameterization.map (planePoint (↑A.parameterization.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * ↑r - 2))) 0)

On the middle piece, the complete replacement path uses its finite PL segment model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.CentralPolygonalArc.completePath_eq_right {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (r : ↑(Set.Icc 0 1)) (hr : 3 / 4 ≤ ↑r) : A.completePath r = (AffineMap.lineMap A.rightEndpoint (G.vertexImage (K.edgeSecond e))) (4 * ↑r - 3)

On the final piece, the complete replacement path is the affine second spoke.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.replacementEdgeMap_edgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : G.replacementEdgeMap e ⟨PlaneGraphRealization.edgePathInSupport e r, ⋯⟩ = (G.replacementArc e).completePath r

Evaluating the edge replacement on its canonical source path recovers the same unit interval parameter on the complete polygonal path.

The finite source breakpoint family

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.rawEdgeMiddleBreakpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.parameterization.source.Vertex) : ℝ

The rawEdgeMiddleBreakpoint declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMiddleBreakpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.parameterization.source.Vertex) : ℝ

The edgeMiddleBreakpoint declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMiddleBreakpoint_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.parameterization.source.Vertex) : edgeMiddleBreakpoint A v ∈ Set.Icc (1 / 2) (3 / 4)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMiddleBreakpoint_eq_raw_of_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.parameterization.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.parameterization.length ≤ A.exitData.right) : edgeMiddleBreakpoint A v = rawEdgeMiddleBreakpoint A v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMiddleSourceScalar_breakpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.parameterization.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.parameterization.length ≤ A.exitData.right) : ↑A.parameterization.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * edgeMiddleBreakpoint A v - 2)) = (A.parameterization.source.position v).ofLp 0

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.EdgeBreakpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Type

The spoke joins and all vertices of the finite middle PL model.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.EdgeBreakpoint A = Option (Option A.parameterization.source.Vertex)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeBreakpointParameter {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (b : EdgeBreakpoint A) : ℝ

The edgeBreakpointParameter declaration.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeBreakpointParameter A none = 1 / 2
• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeBreakpointParameter A (some none) = 3 / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeBreakpointParameter_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (b : EdgeBreakpoint A) : edgeBreakpointParameter A b ∈ Set.Icc 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Plane

The leftSourcePoint declaration.

Equations

• A.leftSourcePoint = LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint (↑A.parameterization.length * A.exitData.left) 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Plane

The rightSourcePoint declaration.

Equations

• A.rightSourcePoint = LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint (↑A.parameterization.length * A.exitData.right) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSourcePoint_mem_source {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftSourcePoint ∈ A.parameterization.source.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightSourcePoint_mem_source {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.rightSourcePoint ∈ A.parameterization.source.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSourcePoint_ne_rightSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftSourcePoint ≠ A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSourcePoint_zero_lt_right {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftSourcePoint.ofLp 0 < A.rightSourcePoint.ofLp 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimMark {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Fin 2 → Plane

The two source points at which the middle polygonal path exits the endpoint disks.

Equations

• A.trimMark ⟨0, isLt⟩ = A.leftSourcePoint
• A.trimMark ⟨1, isLt⟩ = A.rightSourcePoint

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimMark_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimMark 0 = A.leftSourcePoint

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimMark_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimMark 1 = A.rightSourcePoint

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimSubdivision {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : PlaneComplex

The source graph refined at both last-exit points.

Equations

• A.trimSubdivision = A.parameterization.source.markedEdgeSubdivision A.trimMark

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimSource {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : PlaneComplex

The exact closed source interval between the two exits.

Equations

• A.trimSource = A.trimSubdivision.restrictedTo (segment ℝ A.leftSourcePoint A.rightSourcePoint)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimSource_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimSource.support = segment ℝ A.leftSourcePoint A.rightSourcePoint

Marking the two exits makes the interval between them an exact finite subcomplex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : PlaneComplex

Remove the unused vertices retained by restrictedTo.

Equations

• A.trimActive = A.trimSource.active

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimActive.support = segment ℝ A.leftSourcePoint A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive_vertex_mem_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : A.trimActive.Vertex) : A.trimActive.position v ∈ A.trimActive.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive_card_le_two {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (s : Finset A.trimActive.Vertex) : s ∈ A.trimActive.simplexes → s.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive_map_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Set.InjOn A.parameterization.map A.trimActive.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimActive_map_affine {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (s : Finset A.trimActive.Vertex) : s ∈ A.trimActive.simplexes → IsAffineOn A.parameterization.map (A.trimActive.cellCarrier s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimTarget {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : PlaneComplex

The finite target graph carried by the trimmed polygonal middle.

Equations

• A.trimTarget = A.trimActive.mapGraph A.parameterization.map ⋯ ⋯ ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.map_image_sourceSegment {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.parameterization.map '' segment ℝ A.leftSourcePoint A.rightSourcePoint = A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimTarget_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.support = A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftTrimVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.Vertex

The leftTrimVertex declaration.

Equations

• A.leftTrimVertex = Classical.choose ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightTrimVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.Vertex

The rightTrimVertex declaration.

Equations

• A.rightTrimVertex = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftTrimVertex_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : {A.leftTrimVertex} ∈ A.trimTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightTrimVertex_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : {A.rightTrimVertex} ∈ A.trimTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftTrimVertex_sourcePosition {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimActive.position A.leftTrimVertex = A.leftSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightTrimVertex_sourcePosition {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimActive.position A.rightTrimVertex = A.rightSourcePoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.map_leftSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.parameterization.map A.leftSourcePoint = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.map_rightSourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.parameterization.map A.rightSourcePoint = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimTarget_position_left {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.position A.leftTrimVertex = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimTarget_position_right {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.position A.rightTrimVertex = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.isPreconnected_trimTarget_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : IsPreconnected A.trimTarget.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.middleVertexPath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimTarget.vertexGraph.Path A.leftTrimVertex A.rightTrimVertex

A simple finite graph path traversing the trimmed target arc.

Equations

• A.middleVertexPath = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : BrokenLineData Set.univ

An auxiliary broken line which lists the two spokes and every edge and vertex of the trimmed target. Connector segments between listed pieces are harmless: completeTarget below retains only arrangement faces contained in the actual replacement carrier.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain_vertex_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeChain.vertex 0 = G.vertexImage (K.edgeFirst e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain_vertex_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeChain.vertex ⟨1, ⋯⟩ = A.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain_vertex_middle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (i : Fin (A.trimTarget.edgeChain.n + 1)) : A.completeChain.vertex ⟨↑i + 2, ⋯⟩ = A.trimTarget.edgeChain.vertex i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain_vertex_rightEndpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeChain.vertex ⟨A.trimTarget.edgeChain.n + 3, ⋯⟩ = A.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeChain_vertex_finish {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeChain.vertex (Fin.last A.completeChain.n) = G.vertexImage (K.edgeSecond e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeTarget {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : PlaneComplex

The finite plane complex carried by one complete replacement edge.

Equations

• A.completeTarget = A.completeChain.arrangementMesh.toPlaneComplex.restrictedTo A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.exists_completeTarget_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) {x : Plane} (hx : x ∈ A.completeCarrier) : ∃ s ∈ A.completeChain.arrangementMesh.toPlaneComplex.simplexes, x ∈ A.completeChain.arrangementMesh.toPlaneComplex.cellCarrier s ∧ A.completeChain.arrangementMesh.toPlaneComplex.cellCarrier s ⊆ A.completeCarrier ∧ s.card ≤ 2

Every point of a complete replacement edge lies in a one-dimensional arrangement face subordinate to that edge. The cardinality conclusion is what permits several replacement edges to be resolved in one common line arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeTarget_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.support = A.completeCarrier

Exact finite-complex realization of the complete replacement edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeCarrier_subset_segmentCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeCarrier ⊆ A.completeChain.segmentCarrier

Every point of a complete replacement edge lies on one of the finitely listed segments of its auxiliary chain. This is the coverage input used when the three edge chains of a face are placed into one common line arrangement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeStartVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.Vertex

The first intrinsic endpoint as a vertex of the finite complete-edge complex.

Equations

• A.completeStartVertex = A.completeChain.arrangementVertex 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeFinishVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.Vertex

The second intrinsic endpoint as a vertex of the finite complete-edge complex.

Equations

• A.completeFinishVertex = A.completeChain.arrangementVertex (Fin.last A.completeChain.n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeTarget_position_start {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.position A.completeStartVertex = G.vertexImage (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeTarget_position_finish {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.position A.completeFinishVertex = G.vertexImage (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeStartVertex_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : {A.completeStartVertex} ∈ A.completeTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeFinishVertex_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : {A.completeFinishVertex} ∈ A.completeTarget.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.isPreconnected_completeTarget_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : IsPreconnected A.completeTarget.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeVertexPath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeTarget.vertexGraph.Path A.completeStartVertex A.completeFinishVertex

A simple finite graph path whose geometric carrier runs from one abstract endpoint to the other inside the complete replacement edge.

Equations

• A.completeVertexPath = Classical.choice ⋯