Locally finite graph approximation controls

This file begins the noncompact form of Moise Chapter 6, Theorem 2. The finite graph proof uses one minimum separation radius over all vertices and edges. A locally finite complex has no such global minimum. Instead every vertex receives its own positive radius, small enough to avoid all nonincident edges and all other vertices. Local finiteness makes the two obstacle families closed, which is the only compactness input needed for this pointwise construction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_mem_support {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (v : K.Vertex) : K.vertexPoint v ∈ K.support

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) : Type u_1

A realization of the ambient support in an open perturbation region of the plane. The image is allowed to have boundary in that region: in the Rado step it is an open subset of the old polyhedral surface, not an ambiently open plane set. Edge images need only be locally finite in the perturbation region; they may accumulate at its omitted frontier.

• region : Set Plane

  The open plane region in which polygonal perturbations are allowed.

• regionOpen : IsOpen self.region

  The perturbation region is open.

• map : ↑K.support → Plane

  The topological embedding into chart coordinates.

• isEmbedding : Topology.IsEmbedding self.map

  The support is embedded, not merely mapped injectively.

• map_mem_region (p : ↑K.support) : self.map p ∈ self.region

  The original realization lies in the region where perturbations are allowed.

• vertexApproximationControl : K.Vertex → ℝ

  A positive upper bound for the disk chosen at each graph vertex.

• vertexApproximationControl_pos (v : K.Vertex) : 0 < self.vertexApproximationControl v

  Every requested vertex control is positive.

• edgeApproximationControl : K.Edge → ℝ

  A positive upper bound for the central perturbation tube of each graph edge.

• edgeApproximationControl_pos (e : K.Edge) : 0 < self.edgeApproximationControl e

  Every requested edge control is positive.

• mapClosedInRegion : IsClosed (Set.range fun (p : ↑K.support) => ⟨self.map p, ⋯⟩)

  The embedded support is closed relative to the perturbation region. It may still accumulate at the omitted frontier of that region.

• edgeLocallyFinite : LocallyFinite fun (e : K.Edge) => {q : ↑self.region | ↑q ∈ self.map '' {p : ↑K.support | ↑p ∈ K.edgeCarrier e}}

  Edge images are locally finite in the open perturbation region.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.withApproximationControls {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (vertexControl : K.Vertex → ℝ) (hvertex : ∀ (v : K.Vertex), 0 < vertexControl v) (edgeControl : K.Edge → ℝ) (hedge : ∀ (e : K.Edge), 0 < edgeControl e) : K.PlaneGraphRealization

Reduce the quantitative replacement controls without changing the realized map, its target region, or any local-finiteness data.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.withApproximationControls_region {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (vertexControl : K.Vertex → ℝ) (hvertex : ∀ (v : K.Vertex), 0 < vertexControl v) (edgeControl : K.Edge → ℝ) (hedge : ∀ (e : K.Edge), 0 < edgeControl e) : (G.withApproximationControls vertexControl hvertex edgeControl hedge).region = G.region

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.withApproximationControls_map {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (vertexControl : K.Vertex → ℝ) (hvertex : ∀ (v : K.Vertex), 0 < vertexControl v) (edgeControl : K.Edge → ℝ) (hedge : ∀ (e : K.Edge), 0 < edgeControl e) : (G.withApproximationControls vertexControl hvertex edgeControl hedge).map = G.map

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) (p : ↑(K.edgeCarrier e)) : ↑K.support

Include an edge point into the whole support.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeToSupport e p = ⟨↑p, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Plane

The image of a global vertex in chart coordinates.

Equations

• G.vertexImage v = G.map ⟨K.vertexPoint v, ⋯⟩

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

The image of an edge carrier in chart coordinates.

Equations

• G.edgeImage e = G.map '' {p : ↑K.support | ↑p ∈ K.edgeCarrier e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeImage_eq_structure_family {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.edgeImage e = G.map '' {p : ↑K.support | ↑p ∈ K.edgeCarrier e}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeImageInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

One edge image regarded as a subset of the open perturbation region.

Equations

• G.edgeImageInRange e = {q : ↑G.region | ↑q ∈ G.edgeImage e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_edgeImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.edgeImageInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_preimage_subtypeVal_of_subset {X : Type u_2} [TopologicalSpace X] {V C : Set X} (hC : IsCompact C) (hCV : C ⊆ V) : IsCompact (Subtype.val ⁻¹' C)

A compact ambient set contained in a subspace remains compact when regarded as a set in that subspace.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_image_isEmbedding_of_isClosed_range {X : Type u_2} {Y : Type u_3} {I : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {A : I → Set X} (hA : LocallyFinite A) {f : X → Y} (hf : Topology.IsEmbedding f) (hclosed : IsClosed (Set.range f)) : LocallyFinite fun (i : I) => f '' A i

A locally finite family remains locally finite after embedding it as a closed subspace. This is the transport used for a Rado overlap inside the open region obtained by deleting the overlap frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Function.Injective G.vertexImage

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_edgeToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Continuous (edgeToSupport e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isEmbedding_edgeToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Topology.IsEmbedding (edgeToSupport e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_edgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsCompact (G.edgeImage e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_edgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.edgeImage e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑K.support

The canonical interval parametrization of an edge, included into the source support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_edgePathInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Continuous (edgePathInSupport e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupport_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Function.Injective (edgePathInSupport e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ↑(Set.Icc 0 1) → Plane

The charted embedded arc carried by one abstract edge.

Equations

• G.chartEdgePath e = G.map ∘ LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupport e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_chartEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Continuous (G.chartEdgePath e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgePath_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Function.Injective (G.chartEdgePath e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.range_chartEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set.range (G.chartEdgePath e) = G.edgeImage e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgePath_mem_edgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (t : ↑(Set.Icc 0 1)) : G.chartEdgePath e t ∈ G.edgeImage e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgePath_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.chartEdgePath e ⟨0, ⋯⟩ = G.vertexImage (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgePath_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.chartEdgePath e ⟨1, ⋯⟩ = G.vertexImage (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_mem_edgeImage_iff {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) (e : K.Edge) : G.vertexImage v ∈ G.edgeImage e ↔ v ∈ ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isPreconnected_edgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsPreconnected (G.edgeImage e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeImage_diam_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : 0 < Metric.diam (G.edgeImage e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.endpointDist_le_edgeImage_diam {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : dist (G.vertexImage (K.edgeFirst e)) (G.vertexImage (K.edgeSecond e)) ≤ Metric.diam (G.edgeImage e)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeBrokenLineApproximation {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (eps : ℝ) : Type

A polygonal replacement of one charted edge inside a prescribed metric neighborhood.

• eps_pos : 0 < eps
• data : BrokenLineData (Metric.thickening eps (G.edgeImage e))

  The data declaration.

• start_eq : self.data.start = G.vertexImage (K.edgeFirst e)
• finish_eq : self.data.finish = G.vertexImage (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_edgeBrokenLineApproximation {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) {eps : ℝ} (heps : 0 < eps) : Nonempty (G.EdgeBrokenLineApproximation e eps)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeBrokenLineApproximation {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) {eps : ℝ} (heps : 0 < eps) : G.EdgeBrokenLineApproximation e eps

The edgeBrokenLineApproximation declaration.

Equations

• G.edgeBrokenLineApproximation e heps = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeBrokenLineApproximation.resolvedCarrier_subset {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} {eps : ℝ} (A : G.EdgeBrokenLineApproximation e eps) : A.data.resolvedCarrier ⊆ Metric.thickening eps (G.edgeImage e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeImage_inter_eq_sharedVertices {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e d : K.Edge} (hed : e ≠ d) : G.edgeImage e ∩ G.edgeImage d = {p : Plane | ∃ v ∈ ↑e, v ∈ ↑d ∧ p = G.vertexImage v}

Exact charted intersection of two distinct abstract edges.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.nonincidentEdgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set Plane

The union of edge images not incident to v.

Equations

• G.nonincidentEdgeImage v = (⋃ (e : { e : K.Edge // v ∉ ↑e }), G.edgeImage ↑e) ∪ G.regionᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_nonincidentEdgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : IsClosed (G.nonincidentEdgeImage v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_not_mem_nonincidentEdgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexImage v ∉ G.nonincidentEdgeImage v

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImageCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set Plane

Singleton chart images of the global vertices.

Equations

• G.vertexImageCarrier v = {G.vertexImage v}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImageCarrierInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set ↑G.region

A singleton vertex image in the open chart range.

Equations

• G.vertexImageCarrierInRange v = {q : ↑G.region | ↑q ∈ G.vertexImageCarrier v}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_vertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.vertexImageCarrierInRange

Local finiteness of vertex images transported to the chart plane. It follows from edge local finiteness because every vertex belongs to an edge of one of its triangular faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_vertex_ne {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (v : K.Vertex) : ∃ (w : K.Vertex), w ≠ v

Every vertex of a triangle complex has another vertex in one of its incident faces.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.otherVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set Plane

The chart images of all vertices other than v.

Equations

• G.otherVertexImages v = (⋃ (w : { w : K.Vertex // w ≠ v }), G.vertexImageCarrier ↑w) ∪ G.regionᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_otherVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : IsClosed (G.otherVertexImages v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_not_mem_otherVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexImage v ∉ G.otherVertexImages v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.otherVertexImages_nonempty {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : (G.otherVertexImages v).Nonempty

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set Plane

Closed geometric obstacles that a vertex neighborhood must avoid: every nonincident edge and every other vertex.

Equations

• G.vertexObstacle v = G.nonincidentEdgeImage v ∪ G.otherVertexImages v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_vertexObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : IsClosed (G.vertexObstacle v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_not_mem_vertexObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexImage v ∉ G.vertexObstacle v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexObstacle_nonempty {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : (G.vertexObstacle v).Nonempty

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : ℝ

A bounded quarter of the distance from a vertex to every nonincident edge and every other vertex. Unlike the finite graph construction, this radius is allowed to vary from vertex to vertex. The upper bound by one preserves local finiteness of the resulting disks.

Equations

• G.vertexIsolationRadius v = min (G.vertexApproximationControl v) (min 1 (Metric.infDist (G.vertexImage v) (G.vertexObstacle v) / 4))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : 0 < G.vertexIsolationRadius v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius_le_control {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexIsolationRadius v ≤ G.vertexApproximationControl v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius_le_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexIsolationRadius v ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius_lt_infDist {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexIsolationRadius v < Metric.infDist (G.vertexImage v) (G.vertexObstacle v)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexDisk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set Plane

The closed disk selected around a charted vertex.

Equations

• G.vertexDisk v = Metric.closedBall (G.vertexImage v) (G.vertexIsolationRadius v)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexDiskInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Set ↑G.region

A selected vertex disk, restricted to the open chart range.

Equations

• G.vertexDiskInRange v = {p : ↑G.region | ↑p ∈ G.vertexDisk v}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_vertexDisk_vertexObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Disjoint (G.vertexDisk v) (G.vertexObstacle v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexDisk_subset_range {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : G.vertexDisk v ⊆ G.region

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_vertexDisk_nonincidentEdgeImage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Disjoint (G.vertexDisk v) (G.nonincidentEdgeImage v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_vertexDisk_otherVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : Disjoint (G.vertexDisk v) (G.otherVertexImages v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_mem_otherVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {v w : K.Vertex} (hvw : w ≠ v) : G.vertexImage w ∈ G.otherVertexImages v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_mem_vertexObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {v w : K.Vertex} (hvw : w ≠ v) : G.vertexImage w ∈ G.vertexObstacle v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexIsolationRadius_le_quarter_dist {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {v w : K.Vertex} (hvw : w ≠ v) : G.vertexIsolationRadius v ≤ dist (G.vertexImage v) (G.vertexImage w) / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_vertexDisks {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {v w : K.Vertex} (hvw : v ≠ w) : Disjoint (G.vertexDisk v) (G.vertexDisk w)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_vertexDisks {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.vertexDiskInRange

The bounded vertex disks remain locally finite in the open chart range.

Pairwise-separated central edge carriers

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

Open endpoint disks removed before independently perturbing the central part of an edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isOpen_edgeEndpointNeighborhood {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsOpen (G.edgeEndpointNeighborhood e)

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

The compact middle of an edge after removing its two open endpoint disks.

Equations

• G.edgeCentralCarrier e = G.edgeImage e \ G.edgeEndpointNeighborhood e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_edgeCentralCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsCompact (G.edgeCentralCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_edgeCentralCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.edgeCentralCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeCentralCarrier_nonempty {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : (G.edgeCentralCarrier e).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.vertexImage_mem_edgeEndpointNeighborhood {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e : K.Edge} {v : K.Vertex} (hve : v ∈ ↑e) : G.vertexImage v ∈ G.edgeEndpointNeighborhood e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e d : K.Edge} (hed : e ≠ d) : Disjoint (G.edgeCentralCarrier e) (G.edgeCentralCarrier d)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeCentralCarrierInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

A central edge carrier in the open chart range.

Equations

• G.edgeCentralCarrierInRange e = {p : ↑G.region | ↑p ∈ G.edgeCentralCarrier e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_edgeCentralCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.edgeCentralCarrierInRange

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

The closed union of all central edge carriers other than e.

Equations

• G.otherEdgeCentralCarriers e = (⋃ (d : { d : K.Edge // d ≠ e }), G.edgeCentralCarrier ↑d) ∪ G.regionᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_otherEdgeCentralCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.otherEdgeCentralCarriers e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralCarrier_other {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Disjoint (G.edgeCentralCarrier e) (G.otherEdgeCentralCarriers e)

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

The locally finite union of vertex disks not incident to a fixed edge.

Equations

• G.nonincidentVertexDisks e = (⋃ (v : { v : K.Vertex // v ∉ ↑e }), G.vertexDisk ↑v) ∪ G.regionᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_nonincidentVertexDisks {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.nonincidentVertexDisks e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralCarrier_nonincidentVertexDisks {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Disjoint (G.edgeCentralCarrier e) (G.nonincidentVertexDisks e)

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

All closed obstacles from which the middle of e must be separated.

Equations

• G.edgeCentralObstacle e = G.otherEdgeCentralCarriers e ∪ G.nonincidentVertexDisks e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_edgeCentralObstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.edgeCentralObstacle e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralCarrier_obstacle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Disjoint (G.edgeCentralCarrier e) (G.edgeCentralObstacle e)

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

A positive lower separation scale from one compact central edge carrier to the closed union of all the others.

Equations

• G.centralSeparationNN e = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralSeparationNN_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : 0 < G.centralSeparationNN e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralSeparationNN_lt_dist {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) {x y : Plane} (hx : x ∈ G.edgeCentralCarrier e) (hy : y ∈ G.edgeCentralObstacle e) : ↑(G.centralSeparationNN e) < dist x y

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

A bounded quarter-separation tube radius for one central edge carrier. The additional endpoint-distance cap is the quantitative ingredient used in Chapter 6: once the charted edge has small diameter, every point of its replacement arc is correspondingly close to that edge.

Equations

• G.centralTubeRadius e = min (G.edgeApproximationControl e) (min (min 1 (↑(G.centralSeparationNN e) / 4)) (dist (G.vertexImage (K.edgeFirst e)) (G.vertexImage (K.edgeSecond e)) / 4))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralTubeRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : 0 < G.centralTubeRadius e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralTubeRadius_le_control {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.centralTubeRadius e ≤ G.edgeApproximationControl e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralTubeRadius_le_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.centralTubeRadius e ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralTubeRadius_le_quarter_endpointDist {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.centralTubeRadius e ≤ dist (G.vertexImage (K.edgeFirst e)) (G.vertexImage (K.edgeSecond e)) / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.four_mul_centralTubeRadius_lt_dist {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e d : K.Edge} (hed : e ≠ d) {x y : Plane} (hx : x ∈ G.edgeCentralCarrier e) (hy : y ∈ G.edgeCentralCarrier d) : 4 * G.centralTubeRadius e < dist x y

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

The open tube in which the central part of edge e may be polygonalized.

Equations

• G.edgeCentralTube e = Metric.thickening (G.centralTubeRadius e) (G.edgeCentralCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralTube_nonincidentVertexDisk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (v : K.Vertex) (hve : v ∉ ↑e) : Disjoint (G.edgeCentralTube e) (G.vertexDisk v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.disjoint_edgeCentralTubes {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e d : K.Edge} (hed : e ≠ d) : Disjoint (G.edgeCentralTube e) (G.edgeCentralTube d)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeCentralTubeInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

A central perturbation tube regarded as a subset of the open chart range.

Equations

• G.edgeCentralTubeInRange e = {p : ↑G.region | ↑p ∈ G.edgeCentralTube e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeCentralTube_subset_range {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.edgeCentralTube e ⊆ G.region

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.centralTubeRadius_le_quarter_infDist_compl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (hcomp : G.regionᶜ.Nonempty) {x : Plane} (hx : x ∈ G.edgeCentralCarrier e) : G.centralTubeRadius e ≤ Metric.infDist x G.regionᶜ / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_edgeCentralTubes {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.edgeCentralTubeInRange

The bounded central tubes remain locally finite in the open chart range.

Last-exit trims and central polygonal arcs

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

A globally defined charted edge curve, clamped to the unit interval.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_chartEdgeCurve {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Continuous (G.chartEdgeCurve e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgeCurve_eq_of_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : G.chartEdgeCurve e t = G.chartEdgePath e ⟨t, ht⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgeCurve_zero {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.chartEdgeCurve e 0 = G.vertexImage (K.edgeFirst e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.chartEdgeCurve_one {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : G.chartEdgeCurve e 1 = G.vertexImage (K.edgeSecond e)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Type

Ordered exits from the two (possibly differently sized) 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 (G.chartEdgeCurve e self.left) (G.vertexImage (K.edgeFirst e)) = G.vertexIsolationRadius (K.edgeFirst e)
• right_on_sphere : dist (G.chartEdgeCurve e self.right) (G.vertexImage (K.edgeSecond e)) = G.vertexIsolationRadius (K.edgeSecond e)
• after_left (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → G.chartEdgeCurve e t ∉ G.vertexDisk (K.edgeFirst e)
• before_right (t : ℝ) : t ∈ Set.Icc 0 1 → self.left < t → t < self.right → G.chartEdgeCurve e t ∉ G.vertexDisk (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_edgeTrimData {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Nonempty (G.EdgeTrimData e)

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

A fixed last-exit trim on every locally finite edge.

Equations

• G.edgeTrim e = Classical.choice ⋯

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : Set Plane

The connected compact subarc between the two selected exits.

Equations

• T.carrier = G.chartEdgeCurve e '' Set.Icc T.left T.right

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.isCompact_carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : IsCompact T.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.isPreconnected_carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : IsPreconnected T.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.left_mem_carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : G.chartEdgeCurve e T.left ∈ T.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.right_mem_carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : G.chartEdgeCurve e T.right ∈ T.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeTrimData.carrier_subset_edgeCentralCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (T : G.EdgeTrimData e) : T.carrier ⊆ G.edgeCentralCarrier e

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.TwoRadiusBoundaryExitData (gamma : ℝ → Plane) (first second : Plane) (firstRadius secondRadius : ℝ) : Type

Ordered exits for an arc whose endpoints lie on boundary circles of possibly different radii. The finite graph layer uses one common radius; local finiteness naturally requires a radius depending on the vertex.

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_twoRadiusBoundaryExitData {gamma : ℝ → Plane} {first second : Plane} {firstRadius secondRadius : ℝ} (hfirstRadius : 0 < firstRadius) (hsecondRadius : 0 < secondRadius) (hcont : ContinuousOn gamma (Set.Icc 0 1)) (hstart : dist (gamma 0) first = firstRadius) (hfinish : dist (gamma 1) second = secondRadius) (hdisjoint : Disjoint (Metric.closedBall first firstRadius) (Metric.closedBall second secondRadius)) : Nonempty (TwoRadiusBoundaryExitData gamma first second firstRadius secondRadius)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.PLArcParameterization (carrier : Set Plane) (start finish : Plane) : Type 1

A finite PL parameterization of a simple polygonal arc. The carrier is deliberately abstract: Chapter 6 can produce it either from a broken line or directly as the PL image of a finely subdivided source interval.

• length : ℕ

  The length declaration.

• length_pos : 0 < self.length
• 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 (↑self.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 (↑self.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 = carrier
• start_eq : self.curve 0 = start
• finish_eq : self.curve 1 = finish

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_plArcParameterization_of_unitSegment (S : PlaneComplex) (hS : S.support = segment ℝ (planePoint 0 0) (planePoint 1 0)) (hgraph : ∀ s ∈ S.simplexes, s.card ≤ 2) {f : Plane → Plane} (hpl : IsPLOn S f) (hinj : Set.InjOn f S.support) : ∃ (P : PLArcParameterization (f '' S.support) (f (planePoint 0 0)) (f (planePoint 1 0))), P.length = 1 ∧ P.map = f

Package a finite PL embedding of the standard unit segment as an abstract PL arc.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentChain : BrokenLineData Set.univ

A one-edge broken line on the standard unit segment.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentComplex : PlaneComplex

The canonical finite graph complex supported on the standard unit segment.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentComplex_support : unitSegmentComplex.support = segment ℝ (planePoint 0 0) (planePoint 1 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentComplex_graph (s : Finset unitSegmentComplex.Vertex) (hs : s ∈ unitSegmentComplex.simplexes) : s.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegment_mem_bounds {p : Plane} (hp : p ∈ unitSegmentComplex.support) : p.ofLp 1 = 0 ∧ 0 ≤ p.ofLp 0 ∧ p.ofLp 0 ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.planePoint_mem_unitSegment {t : ℝ} (ht : t ∈ Set.Icc 0 1) : planePoint t 0 ∈ unitSegmentComplex.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentFirstVertex : unitSegmentComplex.Vertex

The source vertex at the left endpoint of the unit segment.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentSecondVertex : unitSegmentComplex.Vertex

The source vertex at the right endpoint of the unit segment.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentFirstVertex_position : unitSegmentComplex.position unitSegmentFirstVertex = planePoint 0 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.unitSegmentSecondVertex_position : unitSegmentComplex.position unitSegmentSecondVertex = planePoint 1 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.BrokenLineData.exists_plArcParameterization {U : Set Plane} (B : BrokenLineData U) (hne : B.start ≠ B.finish) : Nonempty (PLArcParameterization B.resolvedCarrier B.start B.finish)

The standard finite PL parameterization carried by a loop-resolved broken line.

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

A simple finite PL replacement for one trimmed central arc, inside its pairwise-disjoint tube. The abstract carrier interface also admits the controlled finite approximation used later in Chapter 6.

• carrier : Set Plane

  The carrier declaration.

• start : Plane

  The start declaration.

• finish : Plane

  The finish declaration.

• parameterizationData : PLArcParameterization self.carrier self.start self.finish

  The parameterizationData declaration.

• carrier_subset_tube : self.carrier ⊆ G.edgeCentralTube e
• carrier_subset_edgeConvexHull : self.carrier ⊆ (convexHull ℝ) (G.edgeImage e)
• start_eq : self.start = G.chartEdgeCurve e (G.edgeTrim e).left
• finish_eq : self.finish = G.chartEdgeCurve e (G.edgeTrim e).right
• curve_close (t : ℝ) : t ∈ Set.Icc 0 1 → dist (self.parameterizationData.curve t) (G.chartEdgeCurve e ((G.edgeTrim e).left + ((G.edgeTrim e).right - (G.edgeTrim e).left) * t)) < G.centralTubeRadius e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_centralPolygonalArc {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Nonempty (G.CentralPolygonalArc e)

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

The centralPolygonalArc declaration.

Equations

• G.centralPolygonalArc e = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.resolvedCarrier_subset {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.carrier ⊆ G.edgeCentralTube e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.resolvedCarrier_subset_edgeConvexHull {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.carrier ⊆ (convexHull ℝ) (G.edgeImage e)

The loop-resolved central arc remains in the convex hull of the original edge image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_resolvedCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} (A : G.CentralPolygonalArc e) (B : G.CentralPolygonalArc d) (hed : e ≠ d) : Disjoint A.carrier B.carrier

@[reducible, inline]

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

Compatibility alias for the finite PL parameterization exposed by a central arc.

Equations

• A.Parameterization = LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.PLArcParameterization A.carrier A.start A.finish

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.resolvedWalk_length_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : 0 < A.parameterizationData.length

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

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

The parameterization declaration.

Equations

• A.parameterization = A.parameterizationData

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.exitData {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : TwoRadiusBoundaryExitData A.parameterization.curve (G.vertexImage (K.edgeFirst e)) (G.vertexImage (K.edgeSecond e)) (G.vertexIsolationRadius (K.edgeFirst e)) (G.vertexIsolationRadius (K.edgeSecond e))

Ordered exits of the resolved polygonal arc from the two variable-radius vertex disks.

Equations

• A.exitData = Classical.choice ⋯

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc 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.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimmedCarrier_subset_resolvedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.trimmedCarrier ⊆ A.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimmedCarrier_avoids_first {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxleft : x ≠ A.parameterization.curve A.exitData.left) : x ∉ G.vertexDisk (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimmedCarrier_avoids_second {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) {x : Plane} (hx : x ∈ A.trimmedCarrier) (hxright : x ≠ A.parameterization.curve A.exitData.right) : x ∉ G.vertexDisk (K.edgeSecond e)

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

The leftEndpoint declaration.

Equations

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

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

The rightEndpoint declaration.

Equations

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

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

The leftSpoke declaration.

Equations

• A.leftSpoke = segment ℝ (G.vertexImage (K.edgeFirst e)) A.leftEndpoint

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

The rightSpoke declaration.

Equations

• A.rightSpoke = segment ℝ A.rightEndpoint (G.vertexImage (K.edgeSecond e))

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

The completeCarrier declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftEndpoint_on_sphere {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : dist A.leftEndpoint (G.vertexImage (K.edgeFirst e)) = G.vertexIsolationRadius (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightEndpoint_on_sphere {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : dist A.rightEndpoint (G.vertexImage (K.edgeSecond e)) = G.vertexIsolationRadius (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftEndpoint_mem_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightEndpoint_mem_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.rightEndpoint ∈ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSpoke_subset_vertexDisk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftSpoke ⊆ G.vertexDisk (K.edgeFirst e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightSpoke_subset_vertexDisk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.rightSpoke ⊆ G.vertexDisk (K.edgeSecond e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeCarrier_subset_edgeConvexHull {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeCarrier ⊆ (convexHull ℝ) (G.edgeImage e)

The complete replacement arc stays in the convex hull of the original embedded edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.dist_lt_two_mul_edgeImage_diam {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) {y p : Plane} (hy : y ∈ A.completeCarrier) (hp : p ∈ G.edgeImage e) : dist y p < 2 * Metric.diam (G.edgeImage e)

Every point of the complete polygonal replacement lies within twice the diameter of the original charted edge from every point of that edge. Thus a sufficiently fine source complex turns the setwise tube construction into a pointwise approximation, without choosing a parameter-preserving polygonalization.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSpoke_inter_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.leftSpoke ∩ A.trimmedCarrier = {A.leftEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightSpoke_inter_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.rightSpoke ∩ A.trimmedCarrier = {A.rightEndpoint}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftSpoke_disjoint_rightSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Disjoint A.leftSpoke A.rightSpoke

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

The trimmed resolved middle, with its parameter interval normalized to the unit interval.

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.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.range_middlePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Set.range ⇑A.middlePath = A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.middlePath_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Function.Injective ⇑A.middlePath

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Path (G.vertexImage (K.edgeFirst e)) (G.vertexImage (K.edgeSecond e))

The complete polygonal replacement path of a locally finite abstract edge.

Equations

• A.completePath = (Path.segment (G.vertexImage (K.edgeFirst e)) A.leftEndpoint).trans (A.middlePath.trans (Path.segment A.rightEndpoint (G.vertexImage (K.edgeSecond e))))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.range_completePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Set.range ⇑A.completePath = A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completePath_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : Function.Injective ⇑A.completePath

Each locally finite replacement edge is a simple polygonal path.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.trimmedCarrier B.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.trimmedCarrier_avoids_nonincident {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : K.Vertex) (hve : v ∉ ↑e) : Disjoint (G.vertexDisk v) A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftEndpoint_ne_leftEndpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : A.leftEndpoint ≠ B.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.leftEndpoint_ne_rightEndpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : A.leftEndpoint ≠ B.rightEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightEndpoint_ne_leftEndpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : A.rightEndpoint ≠ B.leftEndpoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.rightEndpoint_ne_rightEndpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : A.rightEndpoint ≠ B.rightEndpoint

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

The leftOpenSpoke declaration.

Equations

• A.leftOpenSpoke = A.leftSpoke \ {G.vertexImage (K.edgeFirst e)}

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

The rightOpenSpoke declaration.

Equations

• A.rightOpenSpoke = A.rightSpoke \ {G.vertexImage (K.edgeSecond e)}

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

The interiorCarrier declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.firstCenter_not_mem_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : G.vertexImage (K.edgeFirst e) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.secondCenter_not_mem_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : G.vertexImage (K.edgeSecond e) ∉ A.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.firstCenter_not_mem_rightSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : G.vertexImage (K.edgeFirst e) ∉ A.rightSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.secondCenter_not_mem_leftSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : G.vertexImage (K.edgeSecond e) ∉ A.leftSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeCarrier_sdiff_endpoints {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) : A.completeCarrier \ {G.vertexImage (K.edgeFirst e), G.vertexImage (K.edgeSecond e)} = A.interiorCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_leftSpoke_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.leftSpoke B.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_rightSpoke_trimmedCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.rightSpoke B.trimmedCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_leftOpenSpoke_leftOpenSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.leftOpenSpoke B.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_leftOpenSpoke_rightOpenSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.leftOpenSpoke B.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_rightOpenSpoke_leftOpenSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.rightOpenSpoke B.leftOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_rightOpenSpoke_rightOpenSpoke {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.rightOpenSpoke B.rightOpenSpoke

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.disjoint_interiorCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : Disjoint A.interiorCarrier B.interiorCarrier

Distinct locally finite replacement edges have disjoint relative interiors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeCarrier_avoids_nonincident {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : K.Vertex) (hve : v ∉ ↑e) : Disjoint (G.vertexDisk v) A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.vertex_mem_completeCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} (A : G.CentralPolygonalArc e) (v : K.Vertex) (hve : v ∈ ↑e) : G.vertexImage v ∈ A.completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.exists_shared_vertex_of_mem_completeCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) {x : Plane} (hx : x ∈ A.completeCarrier) (hx' : x ∈ B.completeCarrier) : ∃ v ∈ ↑e ∩ ↑d, x = G.vertexImage v

Distinct complete replacement edges meet only at images of shared abstract vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.CentralPolygonalArc.completeCarrier_inter_eq_sharedVertices {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e d : K.Edge} {B : G.CentralPolygonalArc d} (A : G.CentralPolygonalArc e) (hed : e ≠ d) : A.completeCarrier ∩ B.completeCarrier = {x : Plane | ∃ v ∈ ↑e, v ∈ ↑d ∧ x = G.vertexImage v}

Strongly-positive edge controls

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Set ↑K.support

The carrier of an abstract edge, included into the whole source support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_edgeInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : IsCompact (edgeInSupport e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeInSupport_nonempty {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : (edgeInSupport e).Nonempty

The assembled locally finite replacement graph

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

The selected complete replacement arc of an abstract edge.

Equations

• G.replacementArc e = G.centralPolygonalArc e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeInSupport_eq_preimage {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : edgeInSupport e = Subtype.val ⁻¹' K.edgeCarrier e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_edgeInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : LocallyFinite edgeInSupport

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.ofIsOpenEmbedding {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : ↑K.support → Plane) (hf : Topology.IsOpenEmbedding f) : K.PlaneGraphRealization

Any open embedding of the support into the plane gives the relative graph realization needed by the locally finite Chapter 6 construction. Local finiteness is transported through the embedding homeomorphism onto its open range.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.ofEmbeddingInOpenRegion {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (V : Set Plane) (hV : IsOpen V) (f : ↑K.support → Plane) (hf : Topology.IsEmbedding f) (hmem : ∀ (p : ↑K.support), f p ∈ V) (hclosed : IsClosed (Set.range fun (p : ↑K.support) => ⟨f p, ⋯⟩)) : K.PlaneGraphRealization

Build a plane graph realization when the source image is closed in a specified open perturbation region. Unlike ofIsOpenEmbedding, this permits the source image itself to have boundary, which is the form used on a Rado chart overlap.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.range_edgePathInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Set.range (edgePathInSupport e) = edgeInSupport e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupportToCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : ↑(Set.Icc 0 1) → ↑(edgeInSupport e)

Restrict the source edge path to its carrier inside the full support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_edgePathInSupportToCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Continuous (edgePathInSupportToCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupportToCarrier_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Function.Injective (edgePathInSupportToCarrier e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupportToCarrier_surjective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Function.Surjective (edgePathInSupportToCarrier e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupportHomeomorph {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ↑(Set.Icc 0 1) ≃ₜ ↑(edgeInSupport e)

The canonical source interval of an edge, inside the support subtype.

Equations

• G.edgePathInSupportHomeomorph e = ⋯.toHomeomorphOfSurjective ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePathInSupportHomeomorph_apply {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑((G.edgePathInSupportHomeomorph e) r) = edgePathInSupport e r

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.replacementEdgeMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ↑(edgeInSupport e) → Plane

The polygonal replacement map on one closed source edge.

Equations

• G.replacementEdgeMap e p = (G.replacementArc e).completePath ((G.edgePathInSupportHomeomorph e).symm p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_replacementEdgeMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Continuous (G.replacementEdgeMap e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.replacementEdgeMap_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Function.Injective (G.replacementEdgeMap e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.range_replacementEdgeMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set.range (G.replacementEdgeMap e) = (G.replacementArc e).completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.replacementEdgeMap_dist_lt_two_mul_edgeImage_diam {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (p : ↑(edgeInSupport e)) : dist (G.replacementEdgeMap e p) (G.map ↑p) < 2 * Metric.diam (G.edgeImage e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.replacementEdgeMap_vertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (v : K.Vertex) (hve : v ∈ ↑e) : G.replacementEdgeMap e ⟨⟨K.vertexPoint v, ⋯⟩, ⋯⟩ = G.vertexImage v

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.oneSkeletonInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : Set ↑K.support

The source one-skeleton as a subspace of the complete support.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.containingEdge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑oneSkeletonInSupport) : K.Edge

A chosen source edge carrying a one-skeleton point.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.containingEdge p = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.mem_edgeInSupport_containingEdge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑oneSkeletonInSupport) : ↑p ∈ edgeInSupport (containingEdge p)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (p : ↑oneSkeletonInSupport) : Plane

Simultaneous polygonal replacement of the locally finite source one-skeleton.

Equations

• G.graphReplacementMap p = G.replacementEdgeMap (LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.containingEdge p) ⟨↑p, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.replacementEdgeMap_eq_on_overlap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {e d : K.Edge} (p : ↑K.support) (hpe : p ∈ edgeInSupport e) (hpd : p ∈ edgeInSupport d) : G.replacementEdgeMap e ⟨p, hpe⟩ = G.replacementEdgeMap d ⟨p, hpd⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMap_eq {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) (p : ↑oneSkeletonInSupport) (hp : ↑p ∈ edgeInSupport e) : G.graphReplacementMap p = G.replacementEdgeMap e ⟨↑p, hp⟩

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : Set ↑oneSkeletonInSupport

The closed source piece contributed by one edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_edgePieces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : LocallyFinite edgePiece

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_edgePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (edgePiece e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_edgePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : IsCompact (edgePiece e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.iUnion_edgePieces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} : ⋃ (e : K.Edge), edgePiece e = Set.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuousOn_graphReplacementMap_edgePiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ContinuousOn G.graphReplacementMap (edgePiece e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Continuous G.graphReplacementMap

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMap_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Function.Injective G.graphReplacementMap

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.finite_incidentEdges {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (v : K.Vertex) : {e : K.Edge | v ∈ ↑e}.Finite

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

The first radial spoke selected for each abstract edge.

Equations

• G.leftSpokeFamily e = (G.replacementArc e).leftSpoke

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

The final radial spoke selected for each abstract edge.

Equations

• G.rightSpokeFamily e = (G.replacementArc e).rightSpoke

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

The trimmed polygonal middle selected for each abstract edge.

Equations

• G.trimmedCarrierFamily e = (G.replacementArc e).trimmedCarrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.leftSpokeFamilyInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

The first radial spokes, regarded as subsets of the open chart range.

Equations

• G.leftSpokeFamilyInRange e = {p : ↑G.region | ↑p ∈ G.leftSpokeFamily e}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.rightSpokeFamilyInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

The final radial spokes, regarded as subsets of the open chart range.

Equations

• G.rightSpokeFamilyInRange e = {p : ↑G.region | ↑p ∈ G.rightSpokeFamily e}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.trimmedCarrierFamilyInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

The trimmed polygonal middles, regarded as subsets of the open chart range.

Equations

• G.trimmedCarrierFamilyInRange e = {p : ↑G.region | ↑p ∈ G.trimmedCarrierFamily e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_leftSpokeFamily {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.leftSpokeFamilyInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_rightSpokeFamily {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.rightSpokeFamilyInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_trimmedCarrierFamily {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.trimmedCarrierFamilyInRange

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.completeCarrierInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : Set ↑G.region

The completeCarrierInRange declaration.

Equations

• G.completeCarrierInRange e = {p : ↑G.region | ↑p ∈ (G.replacementArc e).completeCarrier}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.locallyFinite_completeCarriers {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : LocallyFinite G.completeCarrierInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_completeCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsCompact (G.replacementArc e).completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosed_completeCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : IsClosed (G.replacementArc e).completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.completeCarrier_subset_range {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : (G.replacementArc e).completeCarrier ⊆ G.region

Every complete replacement arc remains inside the open chart range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMap_mem_range {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (p : ↑oneSkeletonInSupport) : G.graphReplacementMap p ∈ G.region

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMapInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (p : ↑oneSkeletonInSupport) : ↑G.region

The simultaneous replacement map with its natural open chart-range codomain.

Equations

• G.graphReplacementMapInRange p = ⟨G.graphReplacementMap p, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_graphReplacementMapInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Continuous G.graphReplacementMapInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.graphReplacementMapInRange_injective {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Function.Injective G.graphReplacementMapInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosedMap_graphReplacementMapInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : IsClosedMap G.graphReplacementMapInRange

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isClosedEmbedding_graphReplacementMapInRange {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Topology.IsClosedEmbedding G.graphReplacementMapInRange

The simultaneous polygonal replacement is closed in the open chart range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isEmbedding_graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Topology.IsEmbedding G.graphReplacementMap

The locally finite replacement graph has the source graph topology in the ambient plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.range_graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Set.range G.graphReplacementMap = ⋃ (e : K.Edge), (G.replacementArc e).completeCarrier

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.IsPhiApproximation {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) (f : ↑K.support → Plane) : Prop

Pointwise closeness to the original chart realization.

Equations

• G.IsPhiApproximation phi f = ∀ (p : ↑K.support), dist (f p) (G.map p) < phi p

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.EdgeImagesControlled {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) : Prop

The edge-mesh condition which converts setwise polygonal tubes into a pointwise control.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isPhiApproximation_graphReplacementMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {phi : ↑K.support → ℝ} (hsmall : G.EdgeImagesControlled phi) (p : ↑oneSkeletonInSupport) : dist (G.graphReplacementMap p) (G.map ↑p) < phi ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_edgeControlLowerBound {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (e : K.Edge) : ∃ (eps : ℝ), 0 < eps ∧ ∀ p ∈ edgeInSupport e, eps ≤ phi p

A strongly-positive tolerance has a positive uniform lower bound on each compact edge, although it need not have a positive lower bound on the whole noncompact complex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeControlRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (e : K.Edge) : ℝ

A fixed positive edgewise control selected from strong positivity.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeControlRadius hphi e = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeControlRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (e : K.Edge) : 0 < edgeControlRadius hphi e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeControlRadius_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (e : K.Edge) {p : ↑K.support} (hp : p ∈ edgeInSupport e) : edgeControlRadius hphi e ≤ phi p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.edgeImagesControlled_of_diam_lt_controlRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (hsmall : ∀ (e : K.Edge), 2 * Metric.diam (G.edgeImage e) < edgeControlRadius hphi e) : G.EdgeImagesControlled phi

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (p : ↑(stdSimplex ℝ ↥(K.faceVertices f))) : ↑K.support

Include a maximal face into the whole source support.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceToSupport f p = ⟨K.faceMap f p, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.continuous_faceToSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : Continuous (faceToSupport f)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : Set ↑K.support

A face carrier as a compact subset of the whole source support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.isCompact_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : IsCompact (faceInSupport f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.exists_faceControlLowerBound {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (f : K.Face) : ∃ (eps : ℝ), 0 < eps ∧ ∀ p ∈ faceInSupport f, eps ≤ phi p

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceControlRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (f : K.Face) : ℝ

A fixed positive facewise control selected from strong positivity.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceControlRadius hphi f = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceControlRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (f : K.Face) : 0 < faceControlRadius hphi f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceControlRadius_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {phi : ↑K.support → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (f : K.Face) {p : ↑K.support} (hp : p ∈ faceInSupport f) : faceControlRadius hphi f ≤ phi p