Polygonal approximation of intrinsic finite graphs

This file ports the source-independent part of Moise Chapter 6, Theorem 2 from plane complexes to canonical barycentric realizations. The target geometry is unchanged: finitely many compact embedded arcs admit uniform disjoint vertex disks and nonincident edge tubes.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.VertexDiskControl (K : IntrinsicTwoComplex) (h : K.realization → Plane) : Type

Uniform target disks around the images of the used intrinsic vertices.

• radius : ℝ

  The radius declaration.

• radius_pos : 0 < self.radius
• vertices_disjoint (v w : K.UsedVertex) : v ≠ w → Disjoint (Metric.closedBall (h (K.vertexPoint v)) self.radius) (Metric.closedBall (h (K.vertexPoint w)) self.radius)
• avoids_nonincident_edge (v : K.UsedVertex) (e : K.Edge) : ↑v ∉ ↑e → Disjoint (Metric.closedBall (h (K.vertexPoint v)) self.radius) (Metric.cthickening self.radius (Set.range (K.mappedEdgePath h e)))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_vertexDiskControl (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) : Nonempty (K.VertexDiskControl h)

The finite uniform vertex-disk construction for an intrinsic embedded graph.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.VertexDiskControl.shrink (K : IntrinsicTwoComplex) {h : K.realization → Plane} (D : K.VertexDiskControl h) (r : ℝ) (hr : 0 < r) (hrD : r ≤ D.radius) : K.VertexDiskControl h

All intrinsic vertex and nonincident-edge separation properties survive shrinking the common target radius.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.VertexDiskControl.shrink K D r hr hrD = { radius := r, radius_pos := hr, vertices_disjoint := ⋯, avoids_nonincident_edge := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_vertexDiskControl_lt (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) {η : ℝ} (hη : 0 < η) : ∃ (D : K.VertexDiskControl h), D.radius < η

Intrinsic vertex-disk controls can be chosen below any prescribed positive radius.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCurve (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) (t : ℝ) : Plane

A globally defined version of an intrinsic mapped edge, clamped to the unit interval.

Equations

• K.edgeCurve h e t = K.mappedEdgePath h e (Set.projIcc 0 1 LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCurve._proof_1 t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_edgeCurve (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (e : K.Edge) : Continuous (K.edgeCurve h e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCurve_eq_of_mem (K : IntrinsicTwoComplex) {h : K.realization → Plane} (e : K.Edge) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : K.edgeCurve h e t = K.mappedEdgePath h e ⟨t, ht⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCurve_zero (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : K.edgeCurve h e 0 = h (K.edgeFirstPoint e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeCurve_one (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : K.edgeCurve h e 1 = h (K.edgeSecondPoint e)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData (K : IntrinsicTwoComplex) (h : K.realization → Plane) (D : K.VertexDiskControl h) (e : K.Edge) : Type

The two ordered circle crossings delimiting the central part of an intrinsic mapped edge.

• left : ℝ

  The left declaration.

• right : ℝ

  The right declaration.

• left_pos : 0 < self.left
• left_lt_right : self.left < self.right
• right_lt_one : self.right < 1
• left_on_sphere : dist (K.edgeCurve h e self.left) (h (K.edgeFirstPoint e)) = D.radius
• right_on_sphere : dist (K.edgeCurve h e self.right) (h (K.edgeSecondPoint e)) = D.radius
• after_left (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → K.edgeCurve h e t ∉ Metric.closedBall (h (K.edgeFirstPoint e)) D.radius
• before_right (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → t < self.right → K.edgeCurve h e t ∉ Metric.closedBall (h (K.edgeSecondPoint e)) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_edgeTrimData (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (D : K.VertexDiskControl h) (e : K.Edge) : Nonempty (K.EdgeTrimData h D e)

Moise's two-sided last-exit construction for an intrinsic edge.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.centralCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {D : K.VertexDiskControl h} {e : K.Edge} (T : K.EdgeTrimData h D e) : Set Plane

The compact middle of an intrinsic edge after removing its two vertex-disk ends.

Equations

• T.centralCarrier = K.edgeCurve h e '' Set.Icc T.left T.right

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.isCompact_centralCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {D : K.VertexDiskControl h} {e : K.Edge} (T : K.EdgeTrimData h D e) (hcont : Continuous h) : IsCompact T.centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.centralCarrier_subset_mapped_openEdge {K : IntrinsicTwoComplex} {h : K.realization → Plane} {D : K.VertexDiskControl h} {e : K.Edge} (T : K.EdgeTrimData h D e) : T.centralCarrier ⊆ K.mappedEdgePath h e '' {r : ↑(Set.Icc 0 1) | 0 < ↑r ∧ ↑r < 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.disjoint_centralCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {D : K.VertexDiskControl h} {e d : K.Edge} {T' : K.EdgeTrimData h D d} (T : K.EdgeTrimData h D e) (hinj : Function.Injective h) (hed : e ≠ d) : Disjoint T.centralCarrier T'.centralCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeTrim (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (D : K.VertexDiskControl h) (e : K.Edge) : K.EdgeTrimData h D e

A chosen last-exit trim for each intrinsic edge.

Equations

• K.edgeTrim hcont D e = Classical.choice ⋯

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralTubeControl (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) : Type

Pairwise-disjoint closed tubes around all trimmed central intrinsic arcs.

• radius : ℝ

  The radius declaration.

• radius_pos : 0 < self.radius
• radius_lt_vertex : self.radius < D.radius
• pairwise_disjoint (e d : K.Edge) : e ≠ d → Disjoint (Metric.cthickening self.radius (K.edgeTrim hcont D e).centralCarrier) (Metric.cthickening self.radius (K.edgeTrim hcont D d).centralCarrier)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_centralTubeControl (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) : Nonempty (K.CentralTubeControl hcont hinj D)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.isPreconnected_centralCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (D : K.VertexDiskControl h) (e : K.Edge) : IsPreconnected (K.edgeTrim hcont D e).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.left_mem_centralCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (D : K.VertexDiskControl h) (e : K.Edge) : K.edgeCurve h e (K.edgeTrim hcont D e).left ∈ (K.edgeTrim hcont D e).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.EdgeTrimData.right_mem_centralCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (D : K.VertexDiskControl h) (e : K.Edge) : K.edgeCurve h e (K.edgeTrim hcont D e).right ∈ (K.edgeTrim hcont D e).centralCarrier

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) : Type

A polygonal replacement for one trimmed central intrinsic arc, kept inside its tube.

• data : BrokenLineData (Metric.thickening C.radius (K.edgeTrim hcont D e).centralCarrier)

  The data declaration.

• start_eq : self.data.start = K.edgeCurve h e (K.edgeTrim hcont D e).left
• finish_eq : self.data.finish = K.edgeCurve h e (K.edgeTrim hcont D e).right

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_centralPolygonalArc (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) : Nonempty (K.CentralPolygonalArc hcont hinj D C e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.centralPolygonalArc (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) : K.CentralPolygonalArc hcont hinj D C e

The centralPolygonalArc declaration.

Equations

• K.centralPolygonalArc hcont hinj D C e = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.resolvedCarrier_subset_tube {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.data.resolvedCarrier ⊆ Metric.thickening C.radius (K.edgeTrim hcont D e).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_resolvedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.data.resolvedCarrier A'.data.resolvedCarrier

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.Parameterization {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Type 1

A simple parameterization of the polygonal replacement, normalized to the unit interval.

• source : PlaneComplex

  The source declaration.

• map : Plane → Plane

  The map declaration.

• curve : ℝ → Plane

  The curve declaration.

• source_support : self.source.support = segment ℝ (planePoint 0 0) (planePoint (↑A.data.resolvedWalk.length) 0)
• map_isPL : IsPLOn self.source self.map
• map_injectiveOn : Set.InjOn self.map self.source.support
• map_affineOn (s : Finset self.source.Vertex) : s ∈ self.source.simplexes → IsAffineOn self.map (self.source.cellCarrier s)
• source_card_le_two (s : Finset self.source.Vertex) : s ∈ self.source.simplexes → s.card ≤ 2
• source_vertex_mem (v : self.source.Vertex) : self.source.position v ∈ self.source.support
• curve_eq (t : ℝ) : self.curve t = self.map (planePoint (↑A.data.resolvedWalk.length * t) 0)
• continuousOn : ContinuousOn self.curve (Set.Icc 0 1)
• injectiveOn : Set.InjOn self.curve (Set.Icc 0 1)
• image_eq : self.curve '' Set.Icc 0 1 = A.data.resolvedCarrier
• start_eq : self.curve 0 = A.data.start
• finish_eq : self.curve 1 = A.data.finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.start_ne_finish {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.data.start ≠ A.data.finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.resolvedWalk_length_pos {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : 0 < A.data.resolvedWalk.length

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.exists_parameterization {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Nonempty A.Parameterization

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.parameterization {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.Parameterization

The parameterization declaration.

Equations

• A.parameterization = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.exitData {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : BoundaryExitData A.parameterization.curve (h (K.edgeFirstPoint e)) (h (K.edgeSecondPoint e)) D.radius

The ordered exits of the polygonal middle from the two endpoint disks.

Equations

• A.exitData = Classical.choice ⋯

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The trimmedCarrier declaration.

Equations

• A.trimmedCarrier = A.parameterization.curve '' Set.Icc A.exitData.left A.exitData.right

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimmedCarrier_subset_resolvedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.trimmedCarrier ⊆ A.data.resolvedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimmedCarrier_avoids_first {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxleft : x ≠ A.parameterization.curve A.exitData.left) : x ∉ Metric.closedBall (h (K.edgeFirstPoint e)) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimmedCarrier_avoids_second {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxright : x ≠ A.parameterization.curve A.exitData.right) : x ∉ Metric.closedBall (h (K.edgeSecondPoint e)) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.trimmedCarrier_avoids_nonincident {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : K.UsedVertex) (hv : ↑v ∉ ↑e) : Disjoint (Metric.closedBall (h (K.vertexPoint v)) D.radius) A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Plane

The leftEndpoint declaration.

Equations

• A.leftEndpoint = A.parameterization.curve A.exitData.left

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Plane

The rightEndpoint declaration.

Equations

• A.rightEndpoint = A.parameterization.curve A.exitData.right

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The leftSpoke declaration.

Equations

• A.leftSpoke = segment ℝ (h (K.edgeFirstPoint e)) A.leftEndpoint

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The rightSpoke declaration.

Equations

• A.rightSpoke = segment ℝ A.rightEndpoint (h (K.edgeSecondPoint e))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The complete replacement carrier of one intrinsic edge.

Equations

• A.completeCarrier = A.leftSpoke ∪ A.trimmedCarrier ∪ A.rightSpoke

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The leftOpenSpoke declaration.

Equations

• A.leftOpenSpoke = A.leftSpoke \ {h (K.edgeFirstPoint e)}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The rightOpenSpoke declaration.

Equations

• A.rightOpenSpoke = A.rightSpoke \ {h (K.edgeSecondPoint e)}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.interiorCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set Plane

The interiorCarrier declaration.

Equations

• A.interiorCarrier = A.leftOpenSpoke ∪ A.trimmedCarrier ∪ A.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftEndpoint_mem_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightEndpoint_mem_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.rightEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftEndpoint_on_sphere {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : dist A.leftEndpoint (h (K.edgeFirstPoint e)) = D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightEndpoint_on_sphere {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : dist A.rightEndpoint (h (K.edgeSecondPoint e)) = D.radius

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.middlePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Path A.leftEndpoint A.rightEndpoint

The trimmed polygonal middle as a path.

Equations

• A.middlePath = { toFun := fun (t : ↑unitInterval) => A.parameterization.curve ((Path.segment A.exitData.left A.exitData.right) t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.range_middlePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set.range ⇑A.middlePath = A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Path (h (K.edgeFirstPoint e)) (h (K.edgeSecondPoint e))

The complete polygonal replacement path for one intrinsic edge.

Equations

• A.completePath = (Path.segment (h (K.edgeFirstPoint e)) A.leftEndpoint).trans (A.middlePath.trans (Path.segment A.rightEndpoint (h (K.edgeSecondPoint e))))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.range_completePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Set.range ⇑A.completePath = A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.middlePath_injective {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Function.Injective ⇑A.middlePath

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.trimmedCarrier A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftEndpoint_ne_leftEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : A.leftEndpoint ≠ A'.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftEndpoint_ne_rightEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : A.leftEndpoint ≠ A'.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightEndpoint_ne_leftEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : A.rightEndpoint ≠ A'.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightEndpoint_ne_rightEndpoint {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : A.rightEndpoint ≠ A'.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSpoke_subset_disk {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftSpoke ⊆ Metric.closedBall (h (K.edgeFirstPoint e)) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightSpoke_subset_disk {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.rightSpoke ⊆ Metric.closedBall (h (K.edgeSecondPoint e)) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSpoke_inter_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.leftSpoke ∩ A.trimmedCarrier = {A.leftEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.rightSpoke_inter_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.rightSpoke ∩ A.trimmedCarrier = {A.rightEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.leftSpoke_disjoint_rightSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Disjoint A.leftSpoke A.rightSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completePath_injective {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : Function.Injective ⇑A.completePath

Every complete intrinsic replacement edge is a simple path.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.firstCenter_not_mem_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : h (K.edgeFirstPoint e) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.secondCenter_not_mem_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : h (K.edgeSecondPoint e) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.firstCenter_not_mem_rightSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : h (K.edgeFirstPoint e) ∉ A.rightSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.secondCenter_not_mem_leftSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : h (K.edgeSecondPoint e) ∉ A.leftSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeCarrier_sdiff_endpoints {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) : A.completeCarrier \ {h (K.edgeFirstPoint e), h (K.edgeSecondPoint e)} = A.interiorCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_leftSpoke_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.leftSpoke A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_rightSpoke_trimmedCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.rightSpoke A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_leftOpenSpoke_leftOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.leftOpenSpoke A'.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_leftOpenSpoke_rightOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.leftOpenSpoke A'.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_rightOpenSpoke_leftOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.rightOpenSpoke A'.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_rightOpenSpoke_rightOpenSpoke {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.rightOpenSpoke A'.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.disjoint_interiorCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) : Disjoint A.interiorCarrier A'.interiorCarrier

Distinct intrinsic replacement edges have disjoint relative interiors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.completeCarrier_avoids_nonincident {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : K.UsedVertex) (hv : ↑v ∉ ↑e) : Disjoint (Metric.closedBall (h (K.vertexPoint v)) D.radius) A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.vertex_mem_completeCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e : K.Edge} (A : K.CentralPolygonalArc hcont hinj D C e) (v : K.UsedVertex) (hv : ↑v ∈ ↑e) : h (K.vertexPoint v) ∈ A.completeCarrier

The image of either abstract endpoint belongs to its replacement edge carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CentralPolygonalArc.exists_shared_vertex_of_mem_completeCarriers {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {e d : K.Edge} {A' : K.CentralPolygonalArc hcont hinj D C d} (A : K.CentralPolygonalArc hcont hinj D C e) (hed : e ≠ d) {x : Plane} (hx : x ∈ A.completeCarrier) (hx' : x ∈ A'.completeCarrier) : ∃ (v : K.UsedVertex), ↑v ∈ ↑e ∩ ↑d ∧ x = h (K.vertexPoint v)

Distinct replacement edges can meet only at the image of an abstract vertex belonging to both edges. This is the exact face-to-face statement behind the polygonal boundary of every intrinsic triangle.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementArc (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) : K.CentralPolygonalArc hcont hinj D C e

The selected polygonal replacement for an intrinsic edge.

Equations

• K.replacementArc hcont hinj D C e = K.centralPolygonalArc hcont hinj D C e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReplacementCarrier_inter_next (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (t : K.Face) (i : ZMod 3) : (K.replacementArc hcont hinj D C (K.faceEdge t i)).completeCarrier ∩ (K.replacementArc hcont hinj D C (K.faceEdge t (i + 1))).completeCarrier = {h (K.vertexPoint (K.faceUsedVertex t (i + 1)))}

Consecutive replacement edges around one intrinsic face meet exactly at the image of their shared cyclic vertex.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsGraphVertexPoint (K : IntrinsicTwoComplex) (x : K.realization) : Prop

A point is an active graph vertex when it is a canonical used-vertex point.

Equations

• K.IsGraphVertexPoint x = ∃ (v : K.UsedVertex), x = K.vertexPoint v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeParameter (K : IntrinsicTwoComplex) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : ↑(Set.Icc 0 1)

The unique unit-interval parameter of a point on an intrinsic edge.

Equations

• K.edgeParameter e x hx = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath_edgeParameter (K : IntrinsicTwoComplex) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : K.edgePath e (K.edgeParameter e x hx) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeParameter_eq_secondCoordinate (K : IntrinsicTwoComplex) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : ↑(K.edgeParameter e x hx) = ↑x (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeParameter_mem_open_of_not_vertex (K : IntrinsicTwoComplex) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) (hnv : ¬K.IsGraphVertexPoint x) : 0 < ↑(K.edgeParameter e x hx) ∧ ↑(K.edgeParameter e x hx) < 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeAt (K : IntrinsicTwoComplex) (x : K.realization) (hx : x ∈ K.oneSkeleton) : K.Edge

A chosen intrinsic edge through a point of the one-skeleton.

Equations

• K.edgeAt x hx = Classical.choose hx

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeAt_spec (K : IntrinsicTwoComplex) (x : K.realization) (hx : x ∈ K.oneSkeleton) : x ∈ K.faceCarrier ↑(K.edgeAt x hx)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) (x : K.realization) : Plane

The edgewise replacement map, expressed on the intrinsic edge carrier.

Equations

• K.edgeReplacementMap hcont hinj D C e x = (K.replacementArc hcont hinj D C e).completePath.extend (↑x (K.edgeSecond e))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_mem_completeCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : K.edgeReplacementMap hcont hinj D C e x ∈ (K.replacementArc hcont hinj D C e).completeCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (x : K.realization) : Plane

Simultaneous replacement of every intrinsic edge. Vertices are handled first, so the definition is independent of the arbitrary chosen incident edge.

Equations

• K.graphReplacementMap hcont hinj D C x = if K.IsGraphVertexPoint x then h x else if hx : x ∈ K.oneSkeleton then K.edgeReplacementMap hcont hinj D C (K.edgeAt x hx) x else h x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_vertex (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (v : K.UsedVertex) : K.graphReplacementMap hcont hinj D C (K.vertexPoint v) = h (K.vertexPoint v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_eq_edge (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : K.graphReplacementMap hcont hinj D C x = K.edgeReplacementMap hcont hinj D C e x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuousOn_graphReplacementMap_faceCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) : ContinuousOn (K.graphReplacementMap hcont hinj D C) (K.faceCarrier ↑e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuousOn_graphReplacementMap_oneSkeleton (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) : ContinuousOn (K.graphReplacementMap hcont hinj D C) K.oneSkeleton

The simultaneous intrinsic edge replacement is continuous on the entire one-skeleton.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_eq_path (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) : K.edgeReplacementMap hcont hinj D C e x = (K.replacementArc hcont hinj D C e).completePath (K.edgeParameter e x hx)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeReplacementMap_mem_interiorCarrier (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) (hnv : ¬K.IsGraphVertexPoint x) : K.edgeReplacementMap hcont hinj D C e x ∈ (K.replacementArc hcont hinj D C e).interiorCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.vertex_image_ne_edgeReplacementMap (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) (v : K.UsedVertex) (e : K.Edge) (x : K.realization) (hx : x ∈ K.faceCarrier ↑e) (hnv : ¬K.IsGraphVertexPoint x) : h (K.vertexPoint v) ≠ K.edgeReplacementMap hcont hinj D C e x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_injectiveOn_oneSkeleton (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) : Set.InjOn (K.graphReplacementMap hcont hinj D C) K.oneSkeleton

The simultaneous intrinsic graph replacement is injective on the one-skeleton.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_isEmbedding_oneSkeleton (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) : Topology.IsEmbedding fun (x : ↑K.oneSkeleton) => K.graphReplacementMap hcont hinj D C ↑x

The topological part of the intrinsic one-skeleton approximation: a continuous embedding assembled from finitely many polygonal edge paths.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.graphReplacementMap_dist_lt_two_mul (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) (hinj : Function.Injective h) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont hinj D) {η : ℝ} (hsmall : ∀ (e : K.Edge), ∀ x ∈ K.faceCarrier ↑e, ∀ y ∈ K.faceCarrier ↑e, dist (h x) (h y) < η) (hD : D.radius < η) (x : K.realization) : x ∈ K.oneSkeleton → dist (K.graphReplacementMap hcont hinj D C x) (h x) < 2 * η

Quantitative control for simultaneous intrinsic edge replacement. The remaining input is the usual fine-mesh condition: the image of each source edge has diameter below η.