Simultaneous polygonalization of finite embedded plane graphs

This file formalizes the separation part of Moise Chapter 6, Theorem 2. The first construction chooses the disjoint circular regions around graph vertices from Moise's Figure 6.1. Later constructions trim each embedded edge at the last exits from those regions and polygonalize the remaining pairwise-disjoint compact arcs.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_pos_uniform_fintype' {I : Type u_1} [Finite I] [Nonempty I] (P : I → ℝ → Prop) (hP : ∀ (i : I), ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → P i δ) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (i : I) (δ : ℝ), 0 < δ → δ < ε → P i δ

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LastExitData (γ : ℝ → Plane) (center : Plane) (radius : ℝ) : Type

The last parameter at which an arc lies in a closed disk.

• parameter : ℝ

  The parameter declaration.

• parameter_mem : self.parameter ∈ Set.Icc 0 1
• parameter_pos : 0 < self.parameter
• parameter_lt_one : self.parameter < 1
• on_sphere : dist (γ self.parameter) center = radius
• after_exit (t : ℝ) : t ∈ Set.Icc 0 1 → self.parameter < t → γ t ∉ Metric.closedBall center radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_lastExitData {γ : ℝ → Plane} {center : Plane} {radius : ℝ} (hradius : 0 < radius) (hcont : ContinuousOn γ (Set.Icc 0 1)) (hstart : γ 0 = center) (hfinish : γ 1 ∉ Metric.closedBall center radius) : Nonempty (LastExitData γ center radius)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.WeakLastExitData (γ : ℝ → Plane) (center : Plane) (radius : ℝ) : Type

A last exit which may occur at the initial endpoint when the arc starts on the sphere.

• parameter : ℝ

  The parameter declaration.

• parameter_mem : self.parameter ∈ Set.Icc 0 1
• parameter_lt_one : self.parameter < 1
• on_sphere : dist (γ self.parameter) center = radius
• after_exit (t : ℝ) : t ∈ Set.Icc 0 1 → self.parameter < t → γ t ∉ Metric.closedBall center radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_weakLastExitData {γ : ℝ → Plane} {center : Plane} {radius : ℝ} : 0 < radius → ∀ (hcont : ContinuousOn γ (Set.Icc 0 1)) (hstart : dist (γ 0) center = radius) (hfinish : γ 1 ∉ Metric.closedBall center radius), Nonempty (WeakLastExitData γ center radius)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TwoSidedExitData (γ : ℝ → Plane) (first second : Plane) (radius : ℝ) : Type

Ordered exits of an arc from two disjoint endpoint disks.

• 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 (γ self.left) first = radius
• right_on_sphere : dist (γ self.right) second = radius
• after_left (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → γ t ∉ Metric.closedBall first radius
• before_right (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → t < self.right → γ t ∉ Metric.closedBall second radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_twoSidedExitData {γ : ℝ → Plane} {first second : Plane} {radius : ℝ} (hradius : 0 < radius) (hcont : ContinuousOn γ (Set.Icc 0 1)) (hstart : γ 0 = first) (hfinish : γ 1 = second) (hdisjoint : Disjoint (Metric.closedBall first radius) (Metric.closedBall second radius)) : Nonempty (TwoSidedExitData γ first second radius)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.BoundaryExitData (γ : ℝ → Plane) (first second : Plane) (radius : ℝ) : Type

Ordered exits for an arc whose endpoints already lie on the two boundary circles.

• left : ℝ

  The left declaration.

• right : ℝ

  The right declaration.

• left_nonneg : 0 ≤ self.left
• left_lt_right : self.left < self.right
• right_le_one : self.right ≤ 1
• left_on_sphere : dist (γ self.left) first = radius
• right_on_sphere : dist (γ self.right) second = radius
• after_left (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → γ t ∉ Metric.closedBall first radius
• before_right (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → t < self.right → γ t ∉ Metric.closedBall second radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_boundaryExitData {γ : ℝ → Plane} {first second : Plane} {radius : ℝ} (hradius : 0 < radius) (hcont : ContinuousOn γ (Set.Icc 0 1)) (hstart : dist (γ 0) first = radius) (hfinish : dist (γ 1) second = radius) (hdisjoint : Disjoint (Metric.closedBall first radius) (Metric.closedBall second radius)) : Nonempty (BoundaryExitData γ first second radius)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.radial_segments_inter {center p q : Plane} {radius : ℝ} (hradius : 0 < radius) (hp : dist p center = radius) (hq : dist q center = radius) (hpq : p ≠ q) : segment ℝ center p ∩ segment ℝ center q = {center}

Radial segments to two distinct points on the same circle meet only at their center.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.eq_endpoint_of_mem_radial_segment {center p x : Plane} {radius : ℝ} (hradius : 0 < radius) (hp : dist p center = radius) (hx : x ∈ segment ℝ center p) (hxsphere : dist x center = radius) : x = p

The only point of a radial segment on its outer circle is its endpoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.disjoint_radial_segments_away_center {center p q : Plane} {radius : ℝ} (hradius : 0 < radius) (hp : dist p center = radius) (hq : dist q center = radius) (hpq : p ≠ q) : Disjoint (segment ℝ center p \ {center}) (segment ℝ center q \ {center})

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.trans_injective_of_range_inter {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ : Path x y) (δ : Path y z) (hγ : Function.Injective ⇑γ) (hδ : Function.Injective ⇑δ) (hinter : Set.range ⇑γ ∩ Set.range ⇑δ = {y}) : Function.Injective ⇑(γ.trans δ)

Concatenating two simple paths whose ranges meet only at their common endpoint is simple.

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

Moise's pairwise-disjoint circular vertex regions, also disjoint from every nonincident embedded edge.

• radius : ℝ

  The radius declaration.

• radius_pos : 0 < self.radius
• vertices_disjoint (v w : K.Vertex) : v ≠ w → Disjoint (Metric.closedBall (h (K.position v)) self.radius) (Metric.closedBall (h (K.position w)) self.radius)
• avoids_nonincident_edge (v : K.Vertex) (e : K.EdgeFace) : v ∉ ↑e → Disjoint (Metric.closedBall (h (K.position v)) self.radius) (Metric.cthickening self.radius (h '' K.cellCarrier ↑e))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeCurve (K : PlaneComplex) (h : Plane → Plane) (i : Fin (Fintype.card K.EdgeFace)) (t : ℝ) : Plane

The edgeCurve declaration.

Equations

• K.edgeCurve h i t = h ((AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edge_lineMap_mem_support (K : PlaneComplex) (i : Fin (Fintype.card K.EdgeFace)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) t ∈ K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeCurve_continuousOn (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (i : Fin (Fintype.card K.EdgeFace)) : ContinuousOn (K.edgeCurve h i) (Set.Icc 0 1)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeCurve_zero (K : PlaneComplex) (h : Plane → Plane) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeCurve h i 0 = h (K.position (K.edgeFirst i))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeCurve_one (K : PlaneComplex) (h : Plane → Plane) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeCurve h i 1 = h (K.position (K.edgeSecond i))

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData (K : PlaneComplex) (h : Plane → Plane) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : Type

The two ordered circle crossings which delimit the central part of an embedded 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 i self.left) (h (K.position (K.edgeFirst i))) = D.radius
• right_on_sphere : dist (K.edgeCurve h i self.right) (h (K.position (K.edgeSecond i))) = D.radius
• after_left (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → K.edgeCurve h i t ∉ Metric.closedBall (h (K.position (K.edgeFirst i))) D.radius
• before_right (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → t < self.right → K.edgeCurve h i t ∉ Metric.closedBall (h (K.position (K.edgeSecond i))) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_vertexDiskControl (K : PlaneComplex) (hvertex : ∀ (v : K.Vertex), {v} ∈ K.simplexes) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) : Nonempty (K.VertexDiskControl h)

The vertex-disk choice in Moise 6.2, Figure 6.1.

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

All separation properties survive shrinking the common vertex radius.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_vertexDiskControl_lt (K : PlaneComplex) (hvertex : ∀ (v : K.Vertex), {v} ∈ K.simplexes) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) {η : ℝ} (hη : 0 < η) : ∃ (D : K.VertexDiskControl h), D.radius < η

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_edgeTrimData (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : Nonempty (K.EdgeTrimData h D i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.openSegments_disjoint_of_ne (K : PlaneComplex) {i j : Fin (Fintype.card K.EdgeFace)} (hij : i ≠ j) : Disjoint (openSegment ℝ (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) (openSegment ℝ (K.position (K.edgeFirst j)) (K.position (K.edgeSecond j)))

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.centralCarrier {K : PlaneComplex} {h : Plane → Plane} {D : K.VertexDiskControl h} {i : Fin (Fintype.card K.EdgeFace)} (T : K.EdgeTrimData h D i) : Set Plane

The centralCarrier declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.isCompact_centralCarrier {K : PlaneComplex} {h : Plane → Plane} {D : K.VertexDiskControl h} {i : Fin (Fintype.card K.EdgeFace)} (T : K.EdgeTrimData h D i) (hcont : ContinuousOn h K.support) : IsCompact T.centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.centralCarrier_subset_image_openSegment {K : PlaneComplex} {h : Plane → Plane} {D : K.VertexDiskControl h} {i : Fin (Fintype.card K.EdgeFace)} (T : K.EdgeTrimData h D i) : T.centralCarrier ⊆ h '' openSegment ℝ (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.disjoint_centralCarrier {K : PlaneComplex} {h : Plane → Plane} {D : K.VertexDiskControl h} {i j : Fin (Fintype.card K.EdgeFace)} {T' : K.EdgeTrimData h D j} (T : K.EdgeTrimData h D i) (hinj : Set.InjOn h K.support) (hij : i ≠ j) : Disjoint T.centralCarrier T'.centralCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeTrim (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : K.EdgeTrimData h D i

The edgeTrim declaration.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralTubeControl (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) : Type

Pairwise-disjoint closed tubes around all trimmed central arcs.

• radius : ℝ

  The radius declaration.

• radius_pos : 0 < self.radius
• radius_lt_vertex : self.radius < D.radius
• pairwise_disjoint (i j : Fin (Fintype.card K.EdgeFace)) : i ≠ j → Disjoint (Metric.cthickening self.radius (K.edgeTrim hcont D i).centralCarrier) (Metric.cthickening self.radius (K.edgeTrim hcont D j).centralCarrier)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_centralTubeControl (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) (D : K.VertexDiskControl h) : Nonempty (K.CentralTubeControl hcont D)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.isPreconnected_centralCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : IsPreconnected (K.edgeTrim hcont D i).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.left_mem_centralCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeCurve h i (K.edgeTrim hcont D i).left ∈ (K.edgeTrim hcont D i).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.EdgeTrimData.right_mem_centralCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeCurve h i (K.edgeTrim hcont D i).right ∈ (K.edgeTrim hcont D i).centralCarrier

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : Type

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

• data : BrokenLineData (Metric.thickening C.radius (K.edgeTrim hcont D i).centralCarrier ∩ (convexHull ℝ) (h '' K.cellCarrier ↑(K.edgeAt i)))

  The data declaration.

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_centralPolygonalArc (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : Nonempty (K.CentralPolygonalArc hcont D C i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.centralPolygonalArc (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : K.CentralPolygonalArc hcont D C i

The centralPolygonalArc declaration.

Equations

• K.centralPolygonalArc hcont D C i = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.resolvedCarrier_subset_tube {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.data.resolvedCarrier ⊆ Metric.thickening C.radius (K.edgeTrim hcont D i).centralCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.resolvedCarrier_subset_edgeConvexHull {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.data.resolvedCarrier ⊆ (convexHull ℝ) (h '' K.cellCarrier ↑(K.edgeAt i))

The loop-resolved middle remains in the convex hull of the original target edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_resolvedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.data.resolvedCarrier A'.data.resolvedCarrier

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.Parameterization {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : 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_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.PlaneComplex.CentralPolygonalArc.start_ne_finish {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.data.start ≠ A.data.finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.resolvedWalk_length_pos {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : 0 < A.data.resolvedWalk.length

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.exists_parameterization {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Nonempty A.Parameterization

The polygonal arc model from Chapter 6.1 gives a continuous injective unit-interval parameterization.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.parameterization {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.Parameterization

The parameterization declaration.

Equations

• A.parameterization = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.exitData {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : BoundaryExitData A.parameterization.curve (h (K.position (K.edgeFirst i))) (h (K.position (K.edgeSecond i))) D.radius

The portion of the polygonal replacement between its ordered exits from the endpoint disks.

Equations

• A.exitData = Classical.choice ⋯

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The trimmedCarrier declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.trimmedCarrier_subset_resolvedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.trimmedCarrier ⊆ A.data.resolvedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.trimmedCarrier_avoids_first {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxleft : x ≠ A.parameterization.curve A.exitData.left) : x ∉ Metric.closedBall (h (K.position (K.edgeFirst i))) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.trimmedCarrier_avoids_second {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxright : x ≠ A.parameterization.curve A.exitData.right) : x ∉ Metric.closedBall (h (K.position (K.edgeSecond i))) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.trimmedCarrier_avoids_nonincident {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : K.Vertex) (hv : v ∉ ↑(K.edgeAt i)) : Disjoint (Metric.closedBall (h (K.position v)) D.radius) A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Plane

The leftEndpoint declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Plane

The rightEndpoint declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The leftSpoke declaration.

Equations

• A.leftSpoke = segment ℝ (h (K.position (K.edgeFirst i))) A.leftEndpoint

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The rightSpoke declaration.

Equations

• A.rightSpoke = segment ℝ A.rightEndpoint (h (K.position (K.edgeSecond i)))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completeCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The complete polygonal replacement of an edge: a radial spoke, the trimmed middle arc, and a second radial spoke.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completeCarrier_subset_edgeConvexHull {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.completeCarrier ⊆ (convexHull ℝ) (h '' K.cellCarrier ↑(K.edgeAt i))

Every complete finite replacement edge stays in the convex hull of its original target edge. In particular, simultaneous finite graph approximation preserves any convex target such as the model half-plane.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The leftOpenSpoke declaration.

Equations

• A.leftOpenSpoke = A.leftSpoke \ {h (K.position (K.edgeFirst i))}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The rightOpenSpoke declaration.

Equations

• A.rightOpenSpoke = A.rightSpoke \ {h (K.position (K.edgeSecond i))}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.interiorCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set Plane

The relative interior of a replacement edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftEndpoint_mem_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.leftEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightEndpoint_mem_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.rightEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftEndpoint_on_sphere {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : dist A.leftEndpoint (h (K.position (K.edgeFirst i))) = D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightEndpoint_on_sphere {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : dist A.rightEndpoint (h (K.position (K.edgeSecond i))) = D.radius

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.middlePath {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Path A.leftEndpoint A.rightEndpoint

The trimmed middle arc 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.PlaneComplex.CentralPolygonalArc.range_middlePath {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set.range ⇑A.middlePath = A.trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completePath {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Path (h (K.position (K.edgeFirst i))) (h (K.position (K.edgeSecond i)))

The full replacement path for an edge.

Equations

• A.completePath = (Path.segment (h (K.position (K.edgeFirst i))) A.leftEndpoint).trans (A.middlePath.trans (Path.segment A.rightEndpoint (h (K.position (K.edgeSecond i)))))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.range_completePath {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Set.range ⇑A.completePath = A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.middlePath_injective {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Function.Injective ⇑A.middlePath

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.trimmedCarrier A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftEndpoint_ne_leftEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : A.leftEndpoint ≠ A'.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftEndpoint_ne_rightEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : A.leftEndpoint ≠ A'.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightEndpoint_ne_leftEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : A.rightEndpoint ≠ A'.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightEndpoint_ne_rightEndpoint {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : A.rightEndpoint ≠ A'.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftSpoke_subset_disk {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.leftSpoke ⊆ Metric.closedBall (h (K.position (K.edgeFirst i))) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightSpoke_subset_disk {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.rightSpoke ⊆ Metric.closedBall (h (K.position (K.edgeSecond i))) D.radius

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftSpoke_inter_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.leftSpoke ∩ A.trimmedCarrier = {A.leftEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.rightSpoke_inter_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.rightSpoke ∩ A.trimmedCarrier = {A.rightEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.leftSpoke_disjoint_rightSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Disjoint A.leftSpoke A.rightSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completePath_injective {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Function.Injective ⇑A.completePath

Every complete replacement edge is a simple path.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.firstCenter_not_mem_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : h (K.position (K.edgeFirst i)) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.secondCenter_not_mem_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : h (K.position (K.edgeSecond i)) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.firstCenter_not_mem_rightSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : h (K.position (K.edgeFirst i)) ∉ A.rightSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.secondCenter_not_mem_leftSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : h (K.position (K.edgeSecond i)) ∉ A.leftSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completeCarrier_sdiff_endpoints {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : A.completeCarrier \ {h (K.position (K.edgeFirst i)), h (K.position (K.edgeSecond i))} = A.interiorCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_leftSpoke_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.leftSpoke A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_rightSpoke_trimmedCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.rightSpoke A'.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_leftOpenSpoke_leftOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.leftOpenSpoke A'.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_leftOpenSpoke_rightOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.leftOpenSpoke A'.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_rightOpenSpoke_leftOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.rightOpenSpoke A'.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_rightOpenSpoke_rightOpenSpoke {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.rightOpenSpoke A'.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.disjoint_interiorCarrier {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i j : Fin (Fintype.card K.EdgeFace)} {A' : K.CentralPolygonalArc hcont D C j} (A : K.CentralPolygonalArc hcont D C i) (hij : i ≠ j) : Disjoint A.interiorCarrier A'.interiorCarrier

Distinct replacement edges have disjoint relative interiors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.CentralPolygonalArc.completeCarrier_avoids_nonincident {K : PlaneComplex} {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : K.Vertex) (hv : v ∉ ↑(K.edgeAt i)) : Disjoint (Metric.closedBall (h (K.position v)) D.radius) A.completeCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.replacementArc (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : K.CentralPolygonalArc hcont D C i

The selected replacement arc for an enumerated edge.

Equations

• K.replacementArc hcont D C i = K.centralPolygonalArc hcont D C i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.rawMiddleBreakpoint (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : A.parameterization.source.Vertex) : ℝ

The rawMiddleBreakpoint declaration.

Equations

• K.rawMiddleBreakpoint A v = (((A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length - A.exitData.left) / (A.exitData.right - A.exitData.left) + 2) / 4

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleSourceScalarMap (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Plane →ᵃ[ℝ] ℝ

The middleSourceScalarMap declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleSourceMap (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) : Plane →ᵃ[ℝ] Plane

The middleSourceMap declaration.

Equations

• K.middleSourceMap A = LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.realAxisAffine.comp (K.middleSourceScalarMap A)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleSourceMap_apply (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (x : Plane) : (K.middleSourceMap A) x = planePoint (↑A.data.resolvedWalk.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * (K.edgeParameter i) x - 2))) 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleBreakpoint (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : A.parameterization.source.Vertex) : ℝ

The middleBreakpoint declaration.

Equations

• K.middleBreakpoint A v = max (1 / 2) (min (3 / 4) (K.rawMiddleBreakpoint A v))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleBreakpoint_mem (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : A.parameterization.source.Vertex) : K.middleBreakpoint A v ∈ Set.Icc (1 / 2) (3 / 4)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleBreakpoint_eq_raw_of_mem (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length ≤ A.exitData.right) : K.middleBreakpoint A v = K.rawMiddleBreakpoint A v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.middleSourceScalar_breakpoint (K : PlaneComplex) {h : Plane → Plane} {hcont : ContinuousOn h K.support} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont D} {i : Fin (Fintype.card K.EdgeFace)} (A : K.CentralPolygonalArc hcont D C i) (v : A.parameterization.source.Vertex) (hv0 : A.exitData.left ≤ (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length) (hv1 : (A.parameterization.source.position v).ofLp 0 / ↑A.data.resolvedWalk.length ≤ A.exitData.right) : ↑A.data.resolvedWalk.length * (A.exitData.left + (A.exitData.right - A.exitData.left) * (4 * K.middleBreakpoint A v - 2)) = (A.parameterization.source.position v).ofLp 0

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.GraphBreakpoint (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : Type

The finite set of all source breakpoints: the two spoke joins and every vertex of every middle PL model.

Equations

• K.GraphBreakpoint hcont D C = ((i : Fin (Fintype.card K.EdgeFace)) × Option (Option (K.replacementArc hcont D C i).parameterization.source.Vertex))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphBreakpointParameter (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (b : K.GraphBreakpoint hcont D C) : ℝ

The graphBreakpointParameter declaration.

Equations

• K.graphBreakpointParameter hcont D C b = match b.snd with | none => 1 / 2 | some none => 3 / 4 | some (some v) => K.middleBreakpoint (K.replacementArc hcont D C b.fst) v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphBreakpointParameter_mem (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (b : K.GraphBreakpoint hcont D C) : K.graphBreakpointParameter hcont D C b ∈ Set.Icc 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphBreakpointPoint (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (b : K.GraphBreakpoint hcont D C) : Plane

The graphBreakpointPoint declaration.

Equations

• K.graphBreakpointPoint hcont D C b = (AffineMap.lineMap (K.position (K.edgeFirst b.fst)) (K.position (K.edgeSecond b.fst))) (K.graphBreakpointParameter hcont D C b)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphBreakpointPoint_mem_support (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (b : K.GraphBreakpoint hcont D C) : K.graphBreakpointPoint hcont D C b ∈ K.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementSubdivision (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : PlaneComplex

The common source subdivision carrying all edgewise PL breakpoints.

Equations

• K.graphReplacementSubdivision hcont D C = K.markedEdgeSubdivision (K.graphBreakpointPoint hcont D C)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementSubdivision_subdivides (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : (K.graphReplacementSubdivision hcont D C).Subdivides K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_graphReplacementSubdivision_vertex (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (b : K.GraphBreakpoint hcont D C) : ∃ (w : (K.graphReplacementSubdivision hcont D C).Vertex), {w} ∈ (K.graphReplacementSubdivision hcont D C).simplexes ∧ (K.graphReplacementSubdivision hcont D C).position w = K.graphBreakpointPoint hcont D C b

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementFace_parameter_side (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) (b : Option (Option (K.replacementArc hcont D C i).parameterization.source.Vertex)) {u : Finset (K.graphReplacementSubdivision hcont D C).Vertex} (hu : u ∈ (K.graphReplacementSubdivision hcont D C).simplexes) : (∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, (K.edgeParameter i) x ≤ K.graphBreakpointParameter hcont D C ⟨i, b⟩) ∨ ∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, K.graphBreakpointParameter hcont D C ⟨i, b⟩ ≤ (K.edgeParameter i) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementFace_piece (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {u : Finset (K.graphReplacementSubdivision hcont D C).Vertex} (hu : u ∈ (K.graphReplacementSubdivision hcont D C).simplexes) : (∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, (K.edgeParameter i) x ≤ 1 / 2) ∨ ((∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, 1 / 2 ≤ (K.edgeParameter i) x) ∧ ∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, (K.edgeParameter i) x ≤ 3 / 4) ∨ ∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, 3 / 4 ≤ (K.edgeParameter i) x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) (x : Plane) : Plane

The replacement map on the affine line carrying one source edge.

Equations

• K.edgeReplacementMap hcont D C i x = (K.replacementArc hcont D C i).completePath.extend ((K.edgeParameter i) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_continuous (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : Continuous (K.edgeReplacementMap hcont D C i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_first (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeReplacementMap hcont D C i (K.position (K.edgeFirst i)) = h (K.position (K.edgeFirst i))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_second (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeReplacementMap hcont D C i (K.position (K.edgeSecond i)) = h (K.position (K.edgeSecond i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_image_cellCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : K.edgeReplacementMap hcont D C i '' K.cellCarrier ↑(K.edgeAt i) = (K.replacementArc hcont D C i).completeCarrier

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsGraphVertexPoint (K : PlaneComplex) (x : Plane) : Prop

The IsGraphVertexPoint declaration.

Equations

• K.IsGraphVertexPoint x = ∃ (v : K.Vertex), {v} ∈ K.simplexes ∧ x = K.position v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeIndexAt (K : PlaneComplex) (x : Plane) (hx : ∃ (i : Fin (Fintype.card K.EdgeFace)), x ∈ K.cellCarrier ↑(K.edgeAt i)) : Fin (Fintype.card K.EdgeFace)

The edgeIndexAt declaration.

Equations

• K.edgeIndexAt x hx = Classical.choose hx

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeIndexAt_spec (K : PlaneComplex) (x : Plane) (hx : ∃ (i : Fin (Fintype.card K.EdgeFace)), x ∈ K.cellCarrier ↑(K.edgeAt i)) : x ∈ K.cellCarrier ↑(K.edgeAt (K.edgeIndexAt x hx))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (x : Plane) : Plane

The simultaneous replacement map. Active graph vertices are handled first; every other point of the graph lies in the open part of a unique edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_vertex (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) {v : K.Vertex} (hv : {v} ∈ K.simplexes) : K.graphReplacementMap hcont D C (K.position v) = h (K.position v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeIndexAt_eq_of_not_vertex (K : PlaneComplex) {x : Plane} (hnv : ¬K.IsGraphVertexPoint x) (hx : ∃ (i : Fin (Fintype.card K.EdgeFace)), x ∈ K.cellCarrier ↑(K.edgeAt i)) (i : Fin (Fintype.card K.EdgeFace)) (hxi : x ∈ K.cellCarrier ↑(K.edgeAt i)) : K.edgeIndexAt x hx = i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_eq_edge (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) {x : Plane} (hnv : ¬K.IsGraphVertexPoint x) (i : Fin (Fintype.card K.EdgeFace)) (hxi : x ∈ K.cellCarrier ↑(K.edgeAt i)) : K.graphReplacementMap hcont D C x = K.edgeReplacementMap hcont D C i x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_eq_edge_on_cellCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) : Set.EqOn (K.graphReplacementMap hcont D C) (K.edgeReplacementMap hcont D C i) (K.cellCarrier ↑(K.edgeAt i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertexPoint_or_exists_edge_of_mem_support (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {x : Plane} (hx : x ∈ K.support) : K.IsGraphVertexPoint x ∨ ∃ (i : Fin (Fintype.card K.EdgeFace)), x ∈ K.cellCarrier ↑(K.edgeAt i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_mem_targetConvexHull (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) {x : Plane} (hx : x ∈ K.support) : K.graphReplacementMap hcont D C x ∈ (convexHull ℝ) (h '' K.support)

The finite simultaneous graph replacement remains in the convex hull of the original target graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_eq_path (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) : K.edgeReplacementMap hcont D C i x = (K.replacementArc hcont D C i).completePath ⟨(K.edgeParameter i) x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_eq_left (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) (ht : (K.edgeParameter i) x ≤ 1 / 2) : K.edgeReplacementMap hcont D C i x = (AffineMap.lineMap (h (K.position (K.edgeFirst i))) (K.replacementArc hcont D C i).leftEndpoint) (2 * (K.edgeParameter i) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_eq_middle (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) (ht0 : 1 / 2 ≤ (K.edgeParameter i) x) (ht1 : (K.edgeParameter i) x ≤ 3 / 4) : K.edgeReplacementMap hcont D C i x = (K.replacementArc hcont D C i).parameterization.map (planePoint (↑(K.replacementArc hcont D C i).data.resolvedWalk.length * ((K.replacementArc hcont D C i).exitData.left + ((K.replacementArc hcont D C i).exitData.right - (K.replacementArc hcont D C i).exitData.left) * (4 * (K.edgeParameter i) x - 2))) 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_eq_right (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) (ht : 3 / 4 ≤ (K.edgeParameter i) x) : K.edgeReplacementMap hcont D C i x = (AffineMap.lineMap (K.replacementArc hcont D C i).rightEndpoint (h (K.position (K.edgeSecond i)))) (4 * (K.edgeParameter i) x - 3)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_affineOn_left (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {E : Set Plane} (hE : E ⊆ K.cellCarrier ↑(K.edgeAt i)) (hle : ∀ x ∈ E, (K.edgeParameter i) x ≤ 1 / 2) : IsAffineOn (K.graphReplacementMap hcont D C) E

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_affineOn_right (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {E : Set Plane} (hE : E ⊆ K.cellCarrier ↑(K.edgeAt i)) (hge : ∀ x ∈ E, 3 / 4 ≤ (K.edgeParameter i) x) : IsAffineOn (K.graphReplacementMap hcont D C) E

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_affineOn_middle (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {u : Finset (K.graphReplacementSubdivision hcont D C).Vertex} (hu : u ∈ (K.graphReplacementSubdivision hcont D C).simplexes) (hui : (K.graphReplacementSubdivision hcont D C).cellCarrier u ⊆ K.cellCarrier ↑(K.edgeAt i)) (hmid0 : ∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, 1 / 2 ≤ (K.edgeParameter i) x) (hmid1 : ∀ x ∈ (K.graphReplacementSubdivision hcont D C).cellCarrier u, (K.edgeParameter i) x ≤ 3 / 4) : IsAffineOn (K.graphReplacementMap hcont D C) ((K.graphReplacementSubdivision hcont D C).cellCarrier u)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_affineOn_subdivision (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (u : Finset (K.graphReplacementSubdivision hcont D C).Vertex) : u ∈ (K.graphReplacementSubdivision hcont D C).simplexes → IsAffineOn (K.graphReplacementMap hcont D C) ((K.graphReplacementSubdivision hcont D C).cellCarrier u)

The simultaneous edge replacement is affine on every face of its named common source subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_isPL (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : IsPLOn K (K.graphReplacementMap hcont D C)

The simultaneous edge replacement is PL on the original graph. All breakpoints of all polygonal middle arcs occur as vertices of one common finite subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.edgeReplacementMap_mem_interiorCarrier (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) (hnv : ¬K.IsGraphVertexPoint x) : K.edgeReplacementMap hcont D C i x ∈ (K.replacementArc hcont D C i).interiorCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.vertex_image_ne_edgeReplacementMap (K : PlaneComplex) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) (v : K.Vertex) (i : Fin (Fintype.card K.EdgeFace)) {x : Plane} (hx : x ∈ K.cellCarrier ↑(K.edgeAt i)) (hnv : ¬K.IsGraphVertexPoint x) : h (K.position v) ≠ K.edgeReplacementMap hcont D C i x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_injectiveOn (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : Set.InjOn (K.graphReplacementMap hcont D C) K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_isPLEmbeddingOn (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) : IsPLEmbeddingOn K (K.graphReplacementMap hcont D C)

Moise's simultaneous polygonal replacement gives a PL embedding of the finite source graph, before imposing a quantitative approximation bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.graphReplacementMap_dist_lt_two_mul (K : PlaneComplex) {h : Plane → Plane} (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (hcont : ContinuousOn h K.support) (D : K.VertexDiskControl h) (C : K.CentralTubeControl hcont D) {η : ℝ} (hsmall : ∀ u ∈ K.simplexes, ∀ x ∈ K.cellCarrier u, ∀ y ∈ K.cellCarrier u, dist (h x) (h y) < η) (hD : D.radius < η) (x : Plane) : x ∈ K.support → dist (K.graphReplacementMap hcont D C x) (h x) < 2 * η

If the image of every source face has diameter below η, and both geometric controls are smaller than η, then simultaneous polygonal replacement moves every graph point by less than 2 * η.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_graph_PL_approximation_facewise (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) {ε : ℝ} (hε : 0 < ε) : ∃ (f : Plane → Plane), IsPLOn K f ∧ Set.InjOn f K.support ∧ (∀ (v : K.Vertex), f (K.position v) = h (K.position v)) ∧ (∀ x ∈ K.support, dist (f x) (h x) < ε) ∧ (∀ x ∈ K.support, f x ∈ (convexHull ℝ) (h '' K.support)) ∧ ∀ (A : Set Plane), (∀ x ∈ A, ∃ s ∈ K.simplexes, x ∈ K.cellCarrier s ∧ K.cellCarrier s ⊆ A) → IsPLOnSet A f

Moise Chapter 6, Theorem 2 for finite plane complexes: after first sampling the source graph finely, simultaneous polygonal replacement gives an arbitrarily close PL embedding and preserves every original vertex value.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_graph_PL_approximation (K : PlaneComplex) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {h : Plane → Plane} (hcont : ContinuousOn h K.support) (hinj : Set.InjOn h K.support) {ε : ℝ} (hε : 0 < ε) : ∃ (f : Plane → Plane), IsPLOn K f ∧ Set.InjOn f K.support ∧ (∀ (v : K.Vertex), f (K.position v) = h (K.position v)) ∧ ∀ x ∈ K.support, dist (f x) (h x) < ε

Moise Chapter 6, Theorem 2 in its conventional interface.