The Radó chart induction

The skeleton of Moise Ch. 8 (the triangulation theorem for 2-manifolds), extended to bordered surfaces as required by the Eval statement.

Moise's proof of Thm. 8.3 (Radó): cover the surface by chart pairs (Thm. 8.1; finitely many, by compactness), and build an increasing sequence of embedded complexes, absorbing one chart core at each step. The step adjusts the new chart's polyhedral disk by a PL approximation (Thm. 6.3, pl_approximation_two_manifold) so that it meets the already-built complex simplicially (conditions (a)-(h) in Moise's proof), and glues (Thm. 7.6).

This file provides the honest objects for that induction:

• PartialTriangulation S — an embedded finite complex that need not cover S; its realization is computed from the combinatorial data exactly as in GeometricTriangulation, so junk witnesses cannot inhabit it;
• MoiseChart S — a disk or half-disk chart with an explicit compact core;
• moise_finite_chart_cover — the finite chart-core cover (Moise Thm. 8.1 plus compactness);
• RadoInvariant and moise_induction_step — the boundary-aware absorption invariant and the complete one-chart step;
• moise_triangulation_of_boundaries — the finite induction and final geometric realization.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation (S : Type u_1) [TopologicalSpace S] : Type (max 1 u_1)

A finite two-dimensional complex embedded in S, not necessarily covering it. The realization is computed from the combinatorial data (as in GeometricTriangulation), so the support of a partial triangulation is a genuine finite polyhedron sitting inside S.

• Vertex : Type

  The (finite) vertex type.

• vertexFintype : Fintype self.Vertex

  The vertex type is finite.

• vertexDecidableEq : DecidableEq self.Vertex

  Vertices have decidable equality.

• faces : Finset (Finset self.Vertex)

  The faces: three-element vertex sets.

• faces_card (t : Finset self.Vertex) : t ∈ self.faces → t.card = 3

  Every face has exactly three vertices.

• embed : ↑(GeometricRealization self.Vertex self.faces) → S

  The embedding of the realization into S.

• isEmbedding : Topology.IsEmbedding self.embed

  embed is a topological embedding.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.toIntrinsic {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : IntrinsicTwoComplex

Forget the ambient embedding and retain the intrinsic finite complex.

Equations

• T.toIntrinsic = { Vertex := T.Vertex, vertexFintype := T.vertexFintype, vertexDecidableEq := T.vertexDecidableEq, faces := T.faces, faces_card := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.toIntrinsic_faces {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : T.toIntrinsic.faces = T.faces

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : Set S

The part of S covered by the partial triangulation.

Equations

• T.support = Set.range T.embed

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.embedIntoDomain {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) {U : Set S} (hU : T.support ⊆ U) : T.toIntrinsic.realization → ↑U

Restrict the ambient embedding to a set known to contain the support.

Equations

• T.embedIntoDomain hU x = ⟨T.embed x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_embedIntoDomain {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) {U : Set S} (hU : T.support ⊆ U) : Topology.IsEmbedding (T.embedIntoDomain hU)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isCompact_support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : IsCompact T.support

The support of a partial triangulation is compact.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.reembed {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (f : T.toIntrinsic.realization → S) (hf : Topology.IsEmbedding f) : PartialTriangulation S

Re-embed the same finite intrinsic complex in the ambient space. This is the bookkeeping operation used after Moise's vanishing chart replacement: only the coordinate embedding changes; the abstract vertices and maximal faces do not.

Equations

• T.reembed f hf = { Vertex := T.Vertex, vertexFintype := T.toIntrinsic.vertexFintype, vertexDecidableEq := T.vertexDecidableEq, faces := T.faces, faces_card := ⋯, embed := f, isEmbedding := hf }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.reembed_toIntrinsic {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (f : T.toIntrinsic.realization → S) (hf : Topology.IsEmbedding f) : (T.reembed f hf).toIntrinsic = T.toIntrinsic

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.reembed_support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (f : T.toIntrinsic.realization → S) (hf : Topology.IsEmbedding f) : (T.reembed f hf).support = Set.range f

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.replaceOnOpen {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (U : Set T.toIntrinsic.realization) (g : T.toIntrinsic.realization → S) (he : Topology.IsEmbedding (frontierGlue U g T.embed)) : PartialTriangulation S

Replace the ambient embedding on a selected part of the intrinsic realization and retain the old embedding outside. The analytic frontier argument is deliberately supplied as an embedding certificate, so this constructor works in the nonmetrized ambient surface.

Equations

• T.replaceOnOpen U g he = T.reembed (LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierGlue U g T.embed) he

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.replaceOnOpen_support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (U : Set T.toIntrinsic.realization) (g : T.toIntrinsic.realization → S) (he : Topology.IsEmbedding (frontierGlue U g T.embed)) : (T.replaceOnOpen U g he).support = g '' U ∪ T.embed '' Uᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.subset_interior_range_frontierGlue_of_fixedOn {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (U : Set ↑(GeometricRealization T.Vertex T.faces)) (g : ↑(GeometricRealization T.Vertex T.faces) → S) {A C : Set S} (hA : A ⊆ interior C) (hC : C ⊆ T.support) (hfix : ∀ (x : ↑(GeometricRealization T.Vertex T.faces)), T.embed x ∈ C → g x = T.embed x) : A ⊆ interior (Set.range (frontierGlue U g T.embed))

A replacement which fixes every old preimage of a closed buffer retains the interior of that buffer in its range. This is the small topological observation that lets the relative straightening preserve all previously absorbed Radó cores without any ambient isotopy.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.subset_interior_range_frontierGlue_of_fixedOn_of_isInteriorPoint {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) [ChartedSpace (EuclideanHalfSpace 2) S] (U : Set ↑(GeometricRealization T.Vertex T.faces)) (g : ↑(GeometricRealization T.Vertex T.faces) → S) (he : Topology.IsEmbedding (frontierGlue U g T.embed)) {A : Set S} (hA : A ⊆ interior T.support) (hAi : ∀ z ∈ A, (modelWithCornersEuclideanHalfSpace 2).IsInteriorPoint z) (hfix : ∀ (x : ↑(GeometricRealization T.Vertex T.faces)), T.embed x ∈ A → g x = T.embed x) : A ⊆ interior (Set.range (frontierGlue U g T.embed))

At ambient-interior points one does not need a neighborhood contained in the fixed set. Pointwise agreement suffices, because invariance of domain makes the corresponding local sheet of the new embedding open. The separate closed-buffer lemma above remains necessary on the manifold boundary.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.restrictFaces {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (p : Finset T.Vertex → Prop) [DecidablePred p] : PartialTriangulation S

Restrict a partial triangulation to a selected finite family of maximal faces.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.restrictFaces_support_subset {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (p : Finset T.Vertex → Prop) [DecidablePred p] : (T.restrictFaces p).support ⊆ T.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.restrictFaces_support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (p : Finset T.Vertex → Prop) [decidableP : DecidablePred p] : (T.restrictFaces p).support = T.embed '' {x : T.toIntrinsic.realization | ∃ t ∈ T.faces, p t ∧ x ∈ T.toIntrinsic.faceCarrier t}

Exact support formula for a finite face restriction.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.refine {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (R : T.toIntrinsic.Subdivision) : PartialTriangulation S

Replace a partial triangulation by a faithful finite intrinsic subdivision.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.refine_toIntrinsic {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (R : T.toIntrinsic.Subdivision) : (T.refine R).toIntrinsic = R.refined

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.refine_support {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (R : T.toIntrinsic.Subdivision) : (T.refine R).support = T.support

Faithful subdivision changes the finite triangulation data but not its ambient support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_refinedSubcomplex_between {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) {C U : Set S} (hC : IsCompact C) (hCT : C ⊆ T.support) (hU : IsOpen U) (hCU : C ⊆ U) : ∃ (R : T.toIntrinsic.Subdivision) (keep : Finset (Finset R.refined.Vertex)), C ⊆ ((T.refine R).restrictFaces fun (t : Finset (T.refine R).Vertex) => t ∈ keep).support ∧ ((T.refine R).restrictFaces fun (t : Finset (T.refine R).Vertex) => t ∈ keep).support ⊆ U

A compact part of a partial triangulation lying in an ambient open set is carried by a finite face restriction of a faithful refinement which still lies in that open set.

This is the finite collar extracted from Moise Ch. 8, Thm. 2. It is the compact ingredient of the Radó step; the full proof additionally needs the noncompact, locally finite collar whose mesh tends to zero at its frontier.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.toGeometricTriangulation {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (hcovers : T.support = Set.univ) : GeometricTriangulation S

A partial triangulation covering all of S is a geometric triangulation. This is the final conversion at the top of the Radó induction.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.edges {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : Finset (Finset T.Vertex)

The edges of a partial triangulation: the two-element subsets of its faces.

Equations

• T.edges = T.faces.biUnion fun (t : Finset T.Vertex) => Finset.powersetCard 2 t

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.IsDualConnected {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) : Prop

The dual graph of the maximal faces of a partial triangulation is connected.

Equations

• T.IsDualConnected = LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.IsDualConnected T.faces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.card_of_mem_edges {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) {e : Finset T.Vertex} (he : e ∈ T.edges) : e.card = 2

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.BoundaryFacewiseRegular {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) [ChartedSpace (EuclideanHalfSpace 2) S] : Prop

On each maximal triangle, the ambient manifold boundary is one exposed simplicial face of dimension at most one.

This is the missing regularity behind the bordered Moise argument. Merely asking for the boundary to be an edge subcomplex permits an interior chord joining two boundary vertices. An arbitrary convex-hull polygonalization can flatten such a chord onto the model boundary. The facewise condition rules that out and is stable under affine subdivision: the pullback of its supporting face to every new triangle is again empty, a vertex, or an edge.

Equations

• T.BoundaryFacewiseRegular = ∀ t ∈ T.faces, ∃ b ⊆ t, b.card ≤ 2 ∧ ∀ x ∈ T.toIntrinsic.faceCarrier t, T.embed x ∈ ModelWithCorners.boundary S ↔ x ∈ T.toIntrinsic.faceCarrier b

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.BoundaryFacewiseRegularEmbedding {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {V : Type u_2} [Fintype V] (F : Finset (Finset V)) (e : ↑(GeometricRealization V F) → S) : Prop

Facewise boundary regularity for an embedding of a raw finite geometric realization.

This is the side-local form used by the gluing theorem. It deliberately mentions only barycentric coordinates, so it transports transparently across vertex relabelings.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.planeComplex_baryEval_coordZero_exposed (K : PlaneComplex) {t : Finset K.Vertex} (ht : t ∈ K.cells) (hnonneg : ∀ v ∈ t, 0 ≤ (K.position v).ofLp 0) : ∃ b ⊆ t, b.card ≤ 2 ∧ ∀ (x : ↑(GeometricRealization K.Vertex K.cells)), (∀ v ∉ t, ↑x v = 0) → ((K.baryEval ↑x).ofLp 0 = 0 ↔ ∀ v ∉ b, ↑x v = 0)

In a nondegenerate affine triangle lying in the closed half-plane, the zero-normal locus is the convex hull of exactly those vertices on the boundary line. Affine independence rules out all three vertices lying on that line, so this is an exposed face of cardinality at most two.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.TriangleMesh.boundaryFacewiseRegularEmbedding_chart {S : Type u_2} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (M : TriangleMesh) (c : MoiseChart S) (hc : c.BoundaryFaithful) (hmodel : M.toPlaneComplex.support ⊆ c.kind.modelRegion) : BoundaryFacewiseRegularEmbedding M.triangles fun (x : ↑(GeometricRealization M.Vertex M.triangles)) => ↑(c.chart.symm (M.coordinateEmbedInto c.kind.modelRegion hmodel x))

The barycentric realization of a plane triangle mesh lying in a boundary-faithful chart is facewise boundary regular.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.boundaryFacewiseRegularEmbedding_congr {S : Type u_2} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {V : Type u_3} [Fintype V] {F : Finset (Finset V)} {e e' : ↑(GeometricRealization V F) → S} (h : BoundaryFacewiseRegularEmbedding F e) (hee : ∀ (x : ↑(GeometricRealization V F)), e' x ∈ ModelWithCorners.boundary S ↔ e x ∈ ModelWithCorners.boundary S) : BoundaryFacewiseRegularEmbedding F e'

Boundary-face regularity depends only on which source points map to the ambient boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.boundaryFacewiseRegularEmbedding_relabel {S : Type u_2} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] [DecidableEq B] (ι : A ↪ B) (F : Finset (Finset A)) (e : ↑(GeometricRealization A F) → S) (h : BoundaryFacewiseRegularEmbedding F e) : BoundaryFacewiseRegularEmbedding (relabelFaceFamily ι F) (e ∘ ⇑(relabelGeometricRealizationHomeomorph ι F).symm)

Facewise boundary regularity is invariant under an injective relabeling of the vertex type.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.IntrinsicTwoComplex.Subdivision.affineIndependent_vertexImages {K : IntrinsicTwoComplex} (R : K.Subdivision) (t : R.refined.Face) : AffineIndependent ℝ fun (v : ↥↑t) => ↑(R.homeo (R.refined.facePoint t v))

The images of the three vertices of a refined face under a faithful affine subdivision are affinely independent in the old barycentric coordinate space.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.IntrinsicTwoComplex.mem_convexHull_unitVectors_of_mem_faceCarrier (K : IntrinsicTwoComplex) (b : Finset K.Vertex) (x : K.realization) (hx : x ∈ K.faceCarrier b) : ↑x ∈ (convexHull ℝ) ↑(Finset.image (fun (v : K.Vertex) => Pi.single v 1) b)

A barycentric point supported on b lies in the convex hull of the corresponding unit coordinate vectors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.boundaryFacewiseRegular_refine {S : Type u_2} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (T : PartialTriangulation S) (hboundary : T.BoundaryFacewiseRegular) (R : T.toIntrinsic.Subdivision) : (T.refine R).BoundaryFacewiseRegular

Facewise boundary regularity survives every faithful affine intrinsic subdivision.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.ofPlaneComplex {S : Type u_2} [TopologicalSpace S] (K : PlaneComplex) (hpure : K.IsPure2) (e : ↑K.support → S) (he : Topology.IsEmbedding e) : PartialTriangulation S

Transport a pure finite plane complex into an ambient space. The abstract realization is identified with the geometric support by barycentric coordinates, then followed by the supplied ambient embedding.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.ofPlaneComplex_support {S : Type u_2} [TopologicalSpace S] (K : PlaneComplex) (hpure : K.IsPure2) (e : ↑K.support → S) (he : Topology.IsEmbedding e) : (ofPlaneComplex K hpure e he).support = Set.range e

The transported plane patch covers exactly the ambient range of its support embedding.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.empty (S : Type u_2) [TopologicalSpace S] : PartialTriangulation S

The empty partial triangulation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.empty_isDualConnected (S : Type u_2) [TopologicalSpace S] : (empty S).IsDualConnected

The empty partial triangulation is vacuously dual-connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.support_eq_empty_of_faces_eq_empty {S : Type u_2} [TopologicalSpace S] (T : PartialTriangulation S) (h : T.faces = ∅) : T.support = ∅

A partial triangulation with no faces covers nothing: its realization is empty.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.empty_support (S : Type u_2) [TopologicalSpace S] : (empty S).support = ∅

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.toPartialTriangulation {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] [T2Space S] : PartialTriangulation S

A finite compatible ambient triangle family is a partial triangulation of the ambient space. Its support is exactly the union of the face carriers.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.toPartialTriangulation_support {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) [Finite K.Face] [T2Space S] : K.toPartialTriangulation.support = K.support

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.partialChartMap {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (T : PartialTriangulation S) (hdom : T.support ⊆ c.domain) : T.toIntrinsic.realization → Plane

The plane embedding of an intrinsic partial triangulation whose support lies in this chart. This is the source embedding consumed by intrinsic PL approximation in the Rado step.

Equations

• c.partialChartMap T hdom x = ↑(c.chart (T.embedIntoDomain hdom x))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isEmbedding_partialChartMap {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (T : PartialTriangulation S) (hdom : T.support ⊆ c.domain) : Topology.IsEmbedding (c.partialChartMap T hdom)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchToModelRegion {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : ↑c.kind.patchComplex.support → ↑c.kind.modelRegion

Include the fixed polygonal model patch into this chart's model region.

Equations

• c.patchToModelRegion x = ⟨↑x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isEmbedding_patchToModelRegion {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : Topology.IsEmbedding c.patchToModelRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchEmbed {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : ↑c.kind.patchComplex.support → S

Embed the fixed polygonal patch into the ambient surface through the inverse chart.

Equations

• c.patchEmbed x = ↑(c.chart.symm (c.patchToModelRegion x))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isEmbedding_patchEmbed {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : Topology.IsEmbedding c.patchEmbed

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : PartialTriangulation S

The concrete finite partial triangulation supplied by one Moise chart.

Equations

• c.patchPartialTriangulation = LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.ofPlaneComplex c.kind.patchComplex ⋯ c.patchEmbed ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_isDualConnected {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.patchPartialTriangulation.IsDualConnected

The concrete partial triangulation supplied by one chart has a connected dual graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_support {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.patchPartialTriangulation.support = Set.range c.patchEmbed

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_embed_mem_domain {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (x : c.patchPartialTriangulation.toIntrinsic.realization) : c.patchPartialTriangulation.embed x ∈ c.domain

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_chart_coord {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (x : c.patchPartialTriangulation.toIntrinsic.realization) : ↑(c.chart ⟨c.patchPartialTriangulation.embed x, ⋯⟩) = c.kind.patchComplex.baryEval ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.BoundaryFaithful.mem_boundary_iff_isModelBoundary {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) [ChartedSpace (EuclideanHalfSpace 2) S] (hc : c.BoundaryFaithful) (y : S) (hy : y ∈ c.domain) : y ∈ ModelWithCorners.boundary S ↔ c.kind.IsModelBoundary ↑(c.chart ⟨y, hy⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.core_subset_patchPartialTriangulation_support {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.core ⊆ c.patchPartialTriangulation.support

The concrete chart patch covers the marked chart core.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchInModelRegion {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : Set ↑c.kind.modelRegion

The model-region subset occupied by the fixed polygonal patch.

Equations

• c.patchInModelRegion = {p : ↑c.kind.modelRegion | ↑p ∈ c.kind.patchComplex.support}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.range_patchToModelRegion {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : Set.range c.patchToModelRegion = c.patchInModelRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_support_eq_chartImage {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.patchPartialTriangulation.support = Subtype.val '' ⇑c.chart.symm '' c.patchInModelRegion

Exact chart-domain description of the transported patch support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.core_subset_interior_patchPartialTriangulation_support {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.core ⊆ interior c.patchPartialTriangulation.support

The marked core lies in the ambient topological interior of the concrete chart patch.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.patchPartialTriangulation_boundaryFacewiseRegular {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) [ChartedSpace (EuclideanHalfSpace 2) S] (hc : c.BoundaryFaithful) : c.patchPartialTriangulation.BoundaryFacewiseRegular

The fixed disk/half-disk patch has no boundary chords. In a half-disk face its boundary face is obtained by deleting the unique positive-normal vertex 1; in a disk face it is empty.

The locally finite old-complex overlap in one chart

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.perturbationRegion (_k : ChartKind) : Set Plane

The open disk in which chart-coordinate perturbations are performed. For a half-disk chart the model region is a closed subset of this disk; the later bordered approximation must preserve that half-disk rather than use the extra side.

Equations

• _k.perturbationRegion = Metric.ball 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelRegionLocallyCompactSpace (k : ChartKind) : LocallyCompactSpace ↑k.modelRegion

A disk or half-disk model is locally compact in its subtype topology.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isOpen_perturbationRegion (k : ChartKind) : IsOpen k.perturbationRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelRegion_subset_perturbationRegion (k : ChartKind) : k.modelRegion ⊆ k.perturbationRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.ball_inter_closure_modelRegion_subset (k : ChartKind) : Metric.ball 0 1 ∩ closure k.modelRegion ⊆ k.modelRegion

Inside the open perturbation disk, the closure of the model region adds nothing: closure only touches the unit sphere and, for a half-disk, the model already contains its edge line.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelInPerturbation (k : ChartKind) : Set ↑k.perturbationRegion

The chart model, regarded as a subset of its open perturbation disk.

Equations

• k.modelInPerturbation = {p : ↑k.perturbationRegion | ↑p ∈ k.modelRegion}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isClosed_modelInPerturbation (k : ChartKind) : IsClosed k.modelInPerturbation

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelToPerturbationRange (k : ChartKind) : ↑k.modelRegion ≃ₜ ↑k.modelInPerturbation

Identify the model-region subtype with its nested closed subtype in the perturbation disk.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelToPerturbation (k : ChartKind) : ↑k.modelRegion → ↑k.perturbationRegion

Include a disk or half-disk model into the open disk used for perturbations.

Equations

• k.modelToPerturbation p = ⟨↑p, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isClosedEmbedding_modelToPerturbation (k : ChartKind) : Topology.IsClosedEmbedding k.modelToPerturbation

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.patchInPerturbation (k : ChartKind) : Set ↑k.perturbationRegion

The fixed finite chart patch, regarded inside the open perturbation disk.

Equations

• k.patchInPerturbation = {p : ↑k.perturbationRegion | ↑p ∈ k.patchComplex.support}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isCompact_patchInPerturbation (k : ChartKind) : IsCompact k.patchInPerturbation

The chart patch remains compact after lifting it to the perturbation-region subtype.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.chartOverlap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Set T.toIntrinsic.realization

The part of the intrinsic realization whose ambient image lies in a Rado chart domain.

Equations

• T.chartOverlap c = T.embed ⁻¹' c.domain

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isOpen_chartOverlap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : IsOpen (T.chartOverlap c)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.chartOverlapToDomain {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.chartOverlap c) → ↑c.domain

Include an overlap point into the chart domain through the old partial triangulation.

Equations

• T.chartOverlapToDomain c x = ⟨T.embed ↑x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_chartOverlapToDomain {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsEmbedding (T.chartOverlapToDomain c)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.chartOverlapMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.chartOverlap c) → Plane

Chart coordinates of the old partial triangulation on the overlap.

Equations

• T.chartOverlapMap c x = ↑(c.chart (T.chartOverlapToDomain c x))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_chartOverlapMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsEmbedding (T.chartOverlapMap c)

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.adaptiveOverlapComplex {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : LocallyFiniteTriangleComplex ↑(T.chartOverlap c)

The adaptive conforming triangulation of the whole old-complex/chart overlap.

Equations

• T.adaptiveOverlapComplex c = T.toIntrinsic.adaptiveLocallyFiniteTriangleComplex (T.chartOverlap c) ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.adaptiveOverlapChartMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.adaptiveOverlapComplex c).support → Plane

Chart coordinates on the support of the adaptive overlap triangulation.

Equations

• T.adaptiveOverlapChartMap c p = T.chartOverlapMap c ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_adaptiveOverlapChartMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsEmbedding (T.adaptiveOverlapChartMap c)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.chartOverlapModelMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.chartOverlap c) → ↑c.kind.modelRegion

The overlap map with the chart model retained as codomain.

Equations

• T.chartOverlapModelMap c x = c.chart (T.chartOverlapToDomain c x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_chartOverlapModelMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsEmbedding (T.chartOverlapModelMap c)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.chartOverlapPerturbationMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.chartOverlap c) → ↑c.kind.perturbationRegion

The overlap map into the open perturbation disk.

Equations

• T.chartOverlapPerturbationMap c = c.kind.modelToPerturbation ∘ T.chartOverlapModelMap c

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isEmbedding_chartOverlapPerturbationMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsEmbedding (T.chartOverlapPerturbationMap c)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isClosedEmbedding_chartOverlapModelMap {S : Type u_1} [TopologicalSpace S] [T2Space S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsClosedEmbedding (T.chartOverlapModelMap c)

The old polyhedral overlap is closed in the chart model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isClosedEmbedding_chartOverlapPerturbationMap {S : Type u_1} [TopologicalSpace S] [T2Space S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsClosedEmbedding (T.chartOverlapPerturbationMap c)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.adaptiveOverlapToOverlap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.adaptiveOverlapComplex c).support → ↑(T.chartOverlap c)

Forget the support proof of the adaptive overlap complex. Coverage makes this a homeomorphism onto the whole overlap, hence a closed embedding.

Equations

• T.adaptiveOverlapToOverlap c = Subtype.val

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isClosedEmbedding_adaptiveOverlapToOverlap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsClosedEmbedding (T.adaptiveOverlapToOverlap c)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.adaptiveOverlapPerturbationMap {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : ↑(T.adaptiveOverlapComplex c).support → ↑c.kind.perturbationRegion

Chart coordinates of the adaptive overlap, with the open perturbation disk retained as codomain.

Equations

• T.adaptiveOverlapPerturbationMap c = T.chartOverlapPerturbationMap c ∘ T.adaptiveOverlapToOverlap c

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isClosedEmbedding_adaptiveOverlapPerturbationMap {S : Type u_1} [TopologicalSpace S] [T2Space S] (T : PartialTriangulation S) (c : MoiseChart S) : Topology.IsClosedEmbedding (T.adaptiveOverlapPerturbationMap c)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.adaptiveOverlapGraphRealization {S : Type u_1} [TopologicalSpace S] [T2Space S] (T : PartialTriangulation S) (c : MoiseChart S) : (T.adaptiveOverlapComplex c).PlaneGraphRealization

The adaptive overlap as the relative plane graph realization used by the locally finite Chapter 6 approximation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.injective_faceVertices_adaptiveOverlapComplex {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) : Function.Injective (T.adaptiveOverlapComplex c).faceVertices

Crossing-weld plan, item 1, first entry condition: distinct faces of the adaptive overlap complex carry distinct vertex triples.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_separating_control_adaptiveOverlap {S : Type u_1} [TopologicalSpace S] [T2Space S] (T : PartialTriangulation S) (c : MoiseChart S) : ∃ (phi : ↑(T.chartOverlap c) → ℝ), StronglyPositiveOn Set.univ phi ∧ LocallyFiniteTriangleComplex.SeparatesVerticesFromFaces (T.adaptiveOverlapGraphRealization c) fun (p : ↑(T.adaptiveOverlapComplex c).support) => regionSafeControl c.kind.perturbationRegion (T.chartOverlapMap c) phi ↑p

Crossing-weld plan, item 1, second entry condition, in honest existential form: a strongly positive tolerance on the chart overlap whose region-safe reduction separates every vertex of the adaptive overlap complex from every face not containing it, in chart coordinates. This is the locally finite analogue of the finite exists_uniform_vertex_face_separation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.disjoint_image_chartOverlap_embed_compl {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) (c : MoiseChart S) {g : T.toIntrinsic.realization → S} (hg : ∀ x ∈ T.chartOverlap c, g x ∈ c.domain) : Disjoint (g '' T.chartOverlap c) (T.embed '' (T.chartOverlap c)ᶜ)

Crossing-weld plan, item 2, disjointness half: a replacement taking its overlap values in the chart domain never collides with the old embedding outside the overlap. Together with range_frontierGlue, this is the crossing-disjointness input of isEmbedding_frontierGlue_of_matches.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_chartMatchingControl_of_metricSpace {S' : Type u_2} [MetricSpace S'] (T : PartialTriangulation S') (c : MoiseChart S') : ∃ (mu : ↑(T.chartOverlap c) → ℝ), StronglyPositiveOn Set.univ mu ∧ ∀ (g' : ↑(T.chartOverlap c) → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S'), (∀ (y : ↑(T.chartOverlap c)), g ↑y = ↑(c.chart.symm (g' y))) → (∀ (y : ↑(T.chartOverlap c)), dist (↑(g' y)) (T.chartOverlapMap c y) ≤ mu y) → MatchesAtFrontier (T.chartOverlap c) g T.embed

Crossing-weld plan, item 2, matching half (Moise's vanishing tolerance). One strongly positive control on the chart overlap such that EVERY chart-coordinate replacement of the old embedding within that control matches the old embedding at the overlap frontier.

The plane-metric reduction regionSafeControl is deliberately not enough here: a C0 chart may shear plane-close points apart near its frontier (compose a chart with the twist (r, θ) ↦ (r, θ + 1/(1-r)) of the disk: a radial displacement of a quarter of the distance to the sphere is torn to unbounded angular displacement). The modulus must therefore be extracted from the chart homeomorphism itself. This is the metric-target version; the surface version exists_chartMatchingControl metrizes the compact second-countable surface and applies it.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_chartMatchingControlOn_of_metricSpace {S' : Type u_2} [MetricSpace S'] (T : PartialTriangulation S') (c : MoiseChart S') (U : Set T.toIntrinsic.realization) (hU : IsOpen U) (hsub : U ⊆ T.chartOverlap c) : ∃ (mu : ↑U → ℝ), StronglyPositiveOn Set.univ mu ∧ ∀ (g' : ↑U → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S'), (∀ (y : ↑U), g ↑y = ↑(c.chart.symm (g' y))) → (∀ (y : ↑U), dist (↑(g' y)) (T.chartOverlapMap c ⟨↑y, ⋯⟩) ≤ mu y) → MatchesAtFrontier U g T.embed ∧ Disjoint (g '' U) (T.embed '' Uᶜ)

Relative form of the chart matching control. On an arbitrary open subset of the chart overlap, one control simultaneously makes the replacement converge to the old embedding at the new frontier and keeps its image disjoint from the unchanged complement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_chartMatchingControl {S : Type u_1} [TopologicalSpace S] [T2Space S] [CompactSpace S] [SecondCountableTopology S] (T : PartialTriangulation S) (c : MoiseChart S) : ∃ (mu : ↑(T.chartOverlap c) → ℝ), StronglyPositiveOn Set.univ mu ∧ ∀ (g' : ↑(T.chartOverlap c) → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S), (∀ (y : ↑(T.chartOverlap c)), g ↑y = ↑(c.chart.symm (g' y))) → (∀ (y : ↑(T.chartOverlap c)), dist (↑(g' y)) (T.chartOverlapMap c y) ≤ mu y) → MatchesAtFrontier (T.chartOverlap c) g T.embed

Crossing-weld plan, item 2, matching half, on the ambient surface. The statement is metric-free; the compact second-countable surface is metrized and the metric-target version is applied at the compatible metric.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation (X : Type u_2) [TopologicalSpace X] (V : Set Plane) : Type (max 1 u_2)

The geometric certificate retained from a controlled chart replacement. Besides the homeomorphism from the source open set, it records that every replacement face is exactly a polygonal closed disk. Keeping this witness exposed is what the final Radó conforming step needs in order to take a finite arrangement near the compact chart patch.

• complex : LocallyFiniteTriangleComplex ↑V

  The complex declaration.

• sourceHomeomorph : X ≃ₜ ↑self.complex.support

  The sourceHomeomorph declaration.

• facePolygon : self.complex.Face → PolygonalCircle

  The facePolygon declaration.

• faceFillingMap : self.complex.Face → Plane → Plane

  The plane map used to fill each abstract source triangle.

• faceMap_eq (f : self.complex.Face) (x : ↑(stdSimplex ℝ ↥(self.complex.faceVertices f))) : ↑(self.complex.faceMap f x) = self.faceFillingMap f ↑((self.complex.facePlaneHomeomorph f) x)

  The ambient face map is the retained filling in standard triangle coordinates.

• faceCertificate (f : self.complex.Face) : Nonempty (FinitePLHomeomorphBetween (self.faceFillingMap f) LocallyFiniteTriangleComplex.standardFaceRegion (self.facePolygon f).closedRegion)

  The filling is genuinely finite PL, so its boundary marks can be pulled back to a finite source subdivision in the relative conforming step.

• faceClosedRegion_subset (f : self.complex.Face) : (self.facePolygon f).closedRegion ⊆ V
• faceCarrier_eq (f : self.complex.Face) : self.complex.faceCarrier f = {q : ↑V | ↑q ∈ (self.facePolygon f).closedRegion}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.sourceFaceSet {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} (Q : PolygonalReplacementPresentation (↑U) V) (f : Q.complex.Face) : Set K.realization

The source points carried by one named polygonal replacement face.

Equations

• Q.sourceFaceSet f = {x : K.realization | ∃ (hx : x ∈ U), ↑(Q.sourceHomeomorph ⟨x, hx⟩) ∈ Q.complex.faceCarrier f}

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas (K : IntrinsicTwoComplex) (U : Set K.realization) (V : Set Plane) (Q : PolygonalReplacementPresentation (↑U) V) : Type 1

Finite-source bookkeeping retained from an adaptive polygonal replacement.

Faces are grouped into finite adaptive tiles. Any finite tile family is represented exactly by a finite family of faces at one common midpoint level of the original intrinsic complex. This is the missing source-side content behind Moise's conditions (f)--(h); keeping it separate from the coordinate presentation lets the finite arrangement machinery remain generic.

• Tile : Type

  The Tile declaration.

• tileDecidableEq : DecidableEq self.Tile
• tile : Q.complex.Face → self.Tile

  The tile declaration.

• tileFaces : self.Tile → Finset Q.complex.Face

  The tileFaces declaration.

• mem_tileFaces (t : self.Tile) (f : Q.complex.Face) : f ∈ self.tileFaces t ↔ self.tile f = t
• sourceTileCarrier : self.Tile → Set K.realization

  The sourceTileCarrier declaration.

• sourceTileCarrier_subset_open (t : self.Tile) : self.sourceTileCarrier t ⊆ U
• sourceTileCarrier_locallyFinite : LocallyFinite fun (t : self.Tile) => {x : ↑U | ↑x ∈ self.sourceTileCarrier t}
• sourceTileCarrier_eq_faces (t : self.Tile) : self.sourceTileCarrier t = ⋃ (f : ↥(self.tileFaces t)), Q.sourceFaceSet ↑f
• sourceFaceParent : Q.complex.Face → K.Face

  An original maximal face containing each retained source fan face.

• sourceFaceSet_subset_parent (f : Q.complex.Face) : Q.sourceFaceSet f ⊆ K.faceCarrier ↑(self.sourceFaceParent f)
• sourceFaceStandardAffine (f : Q.complex.Face) : ∃ (a : Plane →ᵃ[ℝ] K.Vertex → ℝ), ∀ (x : ↑(Q.complex.ClosedFace f)), ↑↑(Q.sourceHomeomorph.symm (LocallyFiniteTriangleComplex.PlaneGraphRealization.faceToSupport f x)) = a ↑((Q.complex.facePlaneHomeomorph f) x)

  Every retained source face has one affine formula in the original intrinsic barycentric coordinates as a function of its standard planar face coordinates.

• commonLevel : Finset self.Tile → ℕ

  The commonLevel declaration.

• levelFaces (F : Finset self.Tile) : Finset (K.LevelFace (self.commonLevel F))

  The levelFaces declaration.

• sourceTiles_eq_levelFaces (F : Finset self.Tile) : ⋃ (t : ↥F), self.sourceTileCarrier ↑t = ⋃ (u : ↥(self.levelFaces F)), K.levelFaceCarrier ↑u

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.sourceFaceMap {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) (f : Q.complex.Face) : ↑(Q.complex.ClosedFace f) → X

The canonical source parametrization of one retained replacement face. It is obtained by pulling the replacement face parametrization back through the presentation homeomorphism, so it uses exactly the same abstract barycentric coordinates as Q.complex.faceMap.

Equations

• Q.sourceFaceMap f = ⇑Q.sourceHomeomorph.symm ∘ LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.PlaneGraphRealization.faceToSupport f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.sourceHomeomorph_sourceFaceMap {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) (f : Q.complex.Face) (x : ↑(Q.complex.ClosedFace f)) : Q.sourceHomeomorph (Q.sourceFaceMap f x) = LocallyFiniteTriangleComplex.PlaneGraphRealization.faceToSupport f x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.isEmbedding_sourceFaceMap {X : Type u_2} [TopologicalSpace X] {V : Set Plane} [T2Space ↑V] (Q : PolygonalReplacementPresentation X V) (f : Q.complex.Face) : Topology.IsEmbedding (Q.sourceFaceMap f)

Each canonical source face parametrization is an embedding.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.sourceFaceMap_eq_iff {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) {f g : Q.complex.Face} {x : ↑(Q.complex.ClosedFace f)} {y : ↑(Q.complex.ClosedFace g)} : Q.sourceFaceMap f x = Q.sourceFaceMap g y ↔ extendFaceCoordinates (Q.complex.faceVertices f) x = extendFaceCoordinates (Q.complex.faceVertices g) y

Two canonical source-face points agree exactly when their zero-extended barycentric coordinates agree. This is the source-side face-to-face law inherited from the retained replacement complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.range_val_sourceFaceMap {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} (Q : PolygonalReplacementPresentation (↑U) V) (f : Q.complex.Face) : (Set.range fun (z : ↑(Q.complex.ClosedFace f)) => ↑(Q.sourceFaceMap f z)) = Q.sourceFaceSet f

The canonical source parametrization has exactly the retained source face as its range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.finite_facesMeeting {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) {C : Set ↑V} (hC : IsCompact C) : {f : Q.complex.Face | (Q.complex.faceCarrier f ∩ C).Nonempty}.Finite

Only finitely many polygonal replacement faces meet a compact chart set. This is the finiteness cut used before passing to the common supporting-line arrangement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.FacesMeeting {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) (C : Set ↑V) : IsCompact C → Type

The finite subtype of replacement faces meeting a specified compact chart set.

Equations

• Q.FacesMeeting C x✝ = ↑{f : Q.complex.Face | (Q.complex.faceCarrier f ∩ C).Nonempty}

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.facesMeetingFintype {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) (C : Set ↑V) (hC : IsCompact C) : Fintype (Q.FacesMeeting C hC)

Equations

• Q.facesMeetingFintype C hC = ⋯.fintype

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.facesMeetingDecidableEq {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) (C : Set ↑V) (hC : IsCompact C) : DecidableEq (Q.FacesMeeting C hC)

Equations

• Q.facesMeetingDecidableEq C hC = Classical.decEq (Q.FacesMeeting C hC)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.support_inter_subset_iUnion_facesMeeting {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) {C : Set ↑V} (hC : IsCompact C) : Q.complex.support ∩ C ⊆ ⋃ (f : Q.FacesMeeting C hC), Q.complex.faceCarrier ↑f

A compact part of a locally finite replacement support is carried by the finitely many faces which meet it. This is the exact compact-to-finite cut used in Moise's condition (b).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.support_inter_subset_selectedClosedRegion {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (Q : PolygonalReplacementPresentation X V) {C : Set ↑V} (hC : IsCompact C) : Q.complex.support ∩ C ⊆ {x : ↑V | ↑x ∈ PolygonalFamily.closedRegion fun (f : Q.FacesMeeting C hC) => Q.facePolygon ↑f}

On the selected finite family, the preceding carrier union is the union of the retained polygonal closed disks.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.PatchFaces {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : Type

The finite replacement faces which meet the fixed chart patch.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.PatchFaces k Q = Q.FacesMeeting k.patchInPerturbation ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tilesMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : Finset A.Tile

The finite family of adaptive source tiles touched by an arbitrary compact coordinate set. This is the relative form needed after deleting the protected old trace: the compact set used in the weld need not be the whole fixed chart patch.

Equations

• A.tilesMeeting C hC = Finset.image (fun (f : Q.FacesMeeting C hC) => A.tile ↑f) Finset.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.mem_tilesMeeting_iff {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (t : A.Tile) : t ∈ A.tilesMeeting C hC ↔ ∃ (f : Q.FacesMeeting C hC), A.tile ↑f = t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceFinsetMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : Finset Q.complex.Face

All replacement fan faces belonging to a tile touched by C.

Equations

• A.tileFaceFinsetMeeting C hC = (A.tilesMeeting C hC).biUnion A.tileFaces

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.TileFacesMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : Type

The TileFacesMeeting declaration.

Equations

• A.TileFacesMeeting C hC = ↥(A.tileFaceFinsetMeeting C hC)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.mem_tileFaceFinsetMeeting_iff {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (f : Q.complex.Face) : f ∈ A.tileFaceFinsetMeeting C hC ↔ ∃ t ∈ A.tilesMeeting C hC, f ∈ A.tileFaces t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.faceMeeting_mem_tileFaceFinsetMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (f : Q.FacesMeeting C hC) : ↑f ∈ A.tileFaceFinsetMeeting C hC

Every face meeting C belongs to the whole-tile closure of the selected family.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourceTilesMeeting_eq_faces {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : ⋃ (t : ↥(A.tilesMeeting C hC)), A.sourceTileCarrier ↑t = ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f

Closing under the adaptive tiles touched by C is exactly the union of their named replacement faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourceTileFacesMeeting_eq_levelFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f = ⋃ (u : ↥(A.levelFaces (A.tilesMeeting C hC))), K.levelFaceCarrier ↑u

The source selected by an arbitrary compact coordinate set is a literal finite subcomplex at one common midpoint level of the original intrinsic triangulation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isCompact_sourceTileFacesMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : IsCompact (⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourceTileFacesMeeting_subset_open {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.coordinatePreimage_subset_sourceTileFacesMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : {x : K.realization | ∃ (hx : x ∈ U), ↑(Q.sourceHomeomorph ⟨x, hx⟩) ∈ C} ⊆ ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f

The coordinate preimage of C is contained in its whole-tile source closure.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTiles {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : Finset A.Tile

The finite family of adaptive source tiles touched by the compact patch. The conforming extension must retain whole tiles, rather than only the individual fan faces which happen to meet the patch.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.mem_patchTiles_iff {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (t : A.Tile) : t ∈ A.patchTiles ↔ ∃ (f : PolygonalReplacementPresentation.PatchFaces k Q), A.tile ↑f = t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTileFaceFinset {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : Finset Q.complex.Face

All replacement fan faces belonging to a tile touched by the patch.

Equations

• A.patchTileFaceFinset = A.patchTiles.biUnion A.tileFaces

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.PatchTileFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : Type

The PatchTileFaces declaration.

Equations

• A.PatchTileFaces = ↥A.patchTileFaceFinset

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.mem_patchTileFaceFinset_iff {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (f : Q.complex.Face) : f ∈ A.patchTileFaceFinset ↔ ∃ t ∈ A.patchTiles, f ∈ A.tileFaces t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchFace_mem_patchTileFaceFinset {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (f : PolygonalReplacementPresentation.PatchFaces k Q) : ↑f ∈ A.patchTileFaceFinset

Every face which meets the patch belongs to the whole-tile closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourcePatchTiles_eq_faces {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : ⋃ (t : ↥A.patchTiles), A.sourceTileCarrier ↑t = ⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f

Closing under touched adaptive tiles changes the finite coordinate family, but its source is still exactly the union of those finitely many named tiles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourcePatchTileFaces_eq_levelFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : ⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f = ⋃ (u : ↥(A.levelFaces A.patchTiles)), K.levelFaceCarrier ↑u

The whole-tile closure is therefore a literal finite subcomplex at one common midpoint level of the original intrinsic triangulation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isCompact_sourcePatchTileFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : IsCompact (⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f)

The tile-closed source selected for the finite weld is compact. This is the compact subpolyhedron on which the later relative boundary extension is allowed to change the old triangulation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourcePatchTileFaces_subset_open {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : ⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f ⊆ U

Every point of the tile-closed source subcomplex still lies in the open region on which the controlled replacement was constructed.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.coordinatePreimage_patch_subset_sourcePatchTileFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : {x : K.realization | ∃ (hx : x ∈ U), ↑(Q.sourceHomeomorph ⟨x, hx⟩) ∈ k.patchInPerturbation} ⊆ ⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f

The whole old trace over the fixed patch is carried by the tile-closed source selection. This is the source-side coverage needed before cutting the old complex along its finite attaching boundary.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchFacePolygon {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : PatchFaces k Q → PolygonalCircle

The polygonal disk belonging to one replacement face meeting the chart patch.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchFacePolygon k Q f = Q.facePolygon ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchComplex_support_subset_arrangementMesh {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : k.patchComplex.support ⊆ (PolygonalFamily.arrangementMesh (patchFacePolygon k Q)).toPlaneComplex.support

The fixed patch lies in the enclosing triangle used for the finite family of all replacement faces which meet it. The point is that every chart patch lies in the unit ball, while PolygonalFamily.enclosingRadius is at least one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.support_inter_patch_subset_closedRegion {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : Q.complex.support ∩ k.patchInPerturbation ⊆ {x : ↑k.perturbationRegion | ↑x ∈ PolygonalFamily.closedRegion (patchFacePolygon k Q)}

The old replacement trace over the fixed patch is contained in the finite polygonal family selected above.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchTriangleMesh (k : ChartKind) : TriangleMesh

The fixed patch as a triangle mesh, for synchronization with the replacement polygons.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchTriangleMesh k = k.patchComplex.toTriangleMesh

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchOldMesh {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : TriangleMesh

The finite old-side coordinate mesh in the common old/patch arrangement.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchNewMesh {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : TriangleMesh

The finite new-patch coordinate mesh in the same common arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchOldMesh_support {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : (patchOldMesh k Q).toPlaneComplex.support = PolygonalFamily.closedRegion (patchFacePolygon k Q)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchNewMesh_support {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) : (patchNewMesh k Q).toPlaneComplex.support = k.patchComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchMeshes_triangle_card {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) (t : Finset (patchOldMesh k Q).Vertex) : t ∈ (patchOldMesh k Q).triangles ∪ (patchNewMesh k Q).triangles → t.card = 3

Both coordinate sides are restrictions of one ambient triangle mesh, so every retained maximal face is a triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchMeshes_joint_edge_valence {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) (e : Finset (patchOldMesh k Q).Vertex) (he : e.card = 2) : {t ∈ (patchOldMesh k Q).triangles ∪ (patchNewMesh k Q).triangles | e ⊆ t}.card ≤ 2

The two finite coordinate sides satisfy the joint surface edge-incidence bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchMeshes_surface_edge_valence {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) (e : Finset (patchOldMesh k Q).Vertex) : (e ∈ ((patchOldMesh k Q).triangles ∪ (patchNewMesh k Q).triangles).biUnion fun (t : Finset (patchOldMesh k Q).Vertex) => Finset.powersetCard 2 t) → {t ∈ (patchOldMesh k Q).triangles ∪ (patchNewMesh k Q).triangles | e ⊆ t}.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchMeshes_coordinateEmbed_eq_iff {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) (x : ↑(GeometricRealization (patchOldMesh k Q).Vertex (patchOldMesh k Q).triangles)) (y : ↑(GeometricRealization (patchNewMesh k Q).Vertex (patchNewMesh k Q).triangles)) : (patchOldMesh k Q).coordinateEmbed x = (patchNewMesh k Q).coordinateEmbed y ↔ ↑x = ↑y

The two coordinate embeddings agree exactly when their common barycentric coordinates do. This is both interface clauses (hagree and hsep) of the later ambient weld, before composing with the chart homeomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.support_subset_modelRegion_of_coordinate {X : Type u_2} [TopologicalSpace X] {V : Set Plane} (k : ChartKind) (Q : PolygonalReplacementPresentation X V) (g' : X → ↑k.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : Q.complex.support ⊆ {z : ↑V | ↑z ∈ k.modelRegion}

If the retained source coordinates land in a closed model region, the whole replacement support does too.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchFaceClosedRegion_subset_modelRegion {X : Type u_2} [TopologicalSpace X] (k : ChartKind) (Q : PolygonalReplacementPresentation X k.perturbationRegion) (g' : X → ↑k.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : PolygonalFamily.closedRegion (patchFacePolygon k Q) ⊆ k.modelRegion

Consequently every selected face polygon used by the finite patch arrangement lies in the chart model, including the half-plane condition in the bordered case.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchOldSurfaceEmbed {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) (g' : X → ↑c.kind.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : ↑(GeometricRealization (patchOldMesh c.kind Q).Vertex (patchOldMesh c.kind Q).triangles) → S

The old finite coordinate side transported back to the ambient surface chart.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchNewSurfaceEmbed {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) : ↑(GeometricRealization (patchNewMesh c.kind Q).Vertex (patchNewMesh c.kind Q).triangles) → S

The synchronized fixed-patch side transported back by the same chart.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.isEmbedding_patchOldSurfaceEmbed {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) (g' : X → ↑c.kind.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : Topology.IsEmbedding (patchOldSurfaceEmbed c Q g' hcoord)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.isEmbedding_patchNewSurfaceEmbed {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) : Topology.IsEmbedding (patchNewSurfaceEmbed c Q)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.patchSurfaceEmbed_eq_iff {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) (g' : X → ↑c.kind.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) (x : ↑(GeometricRealization (patchOldMesh c.kind Q).Vertex (patchOldMesh c.kind Q).triangles)) (y : ↑(GeometricRealization (patchNewMesh c.kind Q).Vertex (patchNewMesh c.kind Q).triangles)) : patchOldSurfaceEmbed c Q g' hcoord x = patchNewSurfaceEmbed c Q y ↔ ↑x = ↑y

After transport by the chart, equality of old- and new-side points is still exactly equality of their common barycentric coordinate functions.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementPresentation.exists_patch_local_weld {X : Type u_2} [TopologicalSpace X] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (Q : PolygonalReplacementPresentation X c.kind.perturbationRegion) (g' : X → ↑c.kind.modelRegion) (hcoord : ∀ (y : X), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ ∀ e ∈ (F₁ ∪ F₂).biUnion fun (t : Finset V) => Finset.powersetCard 2 t, {t ∈ F₁ ∪ F₂ | e ⊆ t}.card ≤ 2

The finite compact part of the crossing construction already has exactly the common-vertex interface consumed by PartialTriangulation.exists_glued. What remains in the global Radó step is to extend its old side over the complement of the selected adaptive faces.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.singlePolygonMesh {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (i : ι) : TriangleMesh

The part of a synchronized arrangement belonging to one named polygon.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.singlePolygonMesh_support {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (i : ι) : (singlePolygonMesh J N i).toPlaneComplex.support = (J i).closedRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.patchComplex_support_subset_arrangementMesh {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) : k.patchComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support

Every fixed chart patch lies in the enclosing arrangement used to synchronize it with an arbitrary finite polygonal family.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchOldMesh {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) : TriangleMesh

The old member of the common arrangement, restricted to the chosen polygonal union.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchNewMesh {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) : TriangleMesh

The fixed chart patch in the same common arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchOldMesh_support {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) : (synchronizedPatchOldMesh k J).toPlaneComplex.support = PolygonalFamily.closedRegion J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchNewMesh_support {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) : (synchronizedPatchNewMesh k J).toPlaneComplex.support = k.patchComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchMeshes_triangle_card {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) (t : Finset (synchronizedPatchOldMesh k J).Vertex) : t ∈ (synchronizedPatchOldMesh k J).triangles ∪ (synchronizedPatchNewMesh k J).triangles → t.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchMeshes_surface_edge_valence {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) (e : Finset (synchronizedPatchOldMesh k J).Vertex) : (e ∈ ((synchronizedPatchOldMesh k J).triangles ∪ (synchronizedPatchNewMesh k J).triangles).biUnion fun (t : Finset (synchronizedPatchOldMesh k J).Vertex) => Finset.powersetCard 2 t) → {t ∈ (synchronizedPatchOldMesh k J).triangles ∪ (synchronizedPatchNewMesh k J).triangles | e ⊆ t}.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchMeshes_coordinateEmbed_eq_iff {ι : Type u_2} [Fintype ι] (k : ChartKind) (J : ι → PolygonalCircle) (x : ↑(GeometricRealization (synchronizedPatchOldMesh k J).Vertex (synchronizedPatchOldMesh k J).triangles)) (y : ↑(GeometricRealization (synchronizedPatchNewMesh k J).Vertex (synchronizedPatchNewMesh k J).triangles)) : (synchronizedPatchOldMesh k J).coordinateEmbed x = (synchronizedPatchNewMesh k J).coordinateEmbed y ↔ ↑x = ↑y

Both restrictions of the synchronized arrangement use literally the same ambient vertex coordinates.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchOldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : ↑(GeometricRealization (synchronizedPatchOldMesh c.kind J).Vertex (synchronizedPatchOldMesh c.kind J).triangles) → S

Transport the finite polygonal member of a synchronized patch weld to the surface.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchNewSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) : ↑(GeometricRealization (synchronizedPatchNewMesh c.kind J).Vertex (synchronizedPatchNewMesh c.kind J).triangles) → S

Transport the fixed-patch member of a synchronized weld by the same chart.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.isEmbedding_synchronizedPatchOldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : Topology.IsEmbedding (synchronizedPatchOldSurfaceEmbed c J hmodel)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.isEmbedding_synchronizedPatchNewSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) : Topology.IsEmbedding (synchronizedPatchNewSurfaceEmbed c J)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.synchronizedPatchSurfaceEmbed_eq_iff {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) (x : ↑(GeometricRealization (synchronizedPatchOldMesh c.kind J).Vertex (synchronizedPatchOldMesh c.kind J).triangles)) (y : ↑(GeometricRealization (synchronizedPatchNewMesh c.kind J).Vertex (synchronizedPatchNewMesh c.kind J).triangles)) : synchronizedPatchOldSurfaceEmbed c J hmodel x = synchronizedPatchNewSurfaceEmbed c J y ↔ ↑x = ↑y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedPatch.exists_synchronizedPatch_local_weld {ι : Type u_2} {S : Type u_3} [TopologicalSpace S] [Finite ι] (c : MoiseChart S) (J : ι → PolygonalCircle) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ ∀ e ∈ (F₁ ∪ F₂).biUnion fun (t : Finset V) => Finset.powersetCard 2 t, {t ∈ F₁ ∪ F₂ | e ⊆ t}.card ≤ 2

Generic finite synchronized weld for a polygonal old-side family and the fixed chart patch.

A synchronized weld against an arbitrary finite target mesh

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.oldMesh {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) : TriangleMesh

The old polygonal member of the common arrangement with an arbitrary finite target mesh.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.newMesh {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) : TriangleMesh

The prescribed finite target member of the same common arrangement.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.newMesh J N = LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetSynchronizedMesh J N

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.oldMesh_support {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) : (oldMesh J N).toPlaneComplex.support = PolygonalFamily.closedRegion J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.newMesh_support {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (hN : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) : (newMesh J N).toPlaneComplex.support = N.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.meshes_triangle_card {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (t : Finset (oldMesh J N).Vertex) : t ∈ (oldMesh J N).triangles ∪ (newMesh J N).triangles → t.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.meshes_surface_edge_valence {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (e : Finset (oldMesh J N).Vertex) : (e ∈ ((oldMesh J N).triangles ∪ (newMesh J N).triangles).biUnion fun (t : Finset (oldMesh J N).Vertex) => Finset.powersetCard 2 t) → {t ∈ (oldMesh J N).triangles ∪ (newMesh J N).triangles | e ⊆ t}.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.meshes_coordinateEmbed_eq_iff {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (x : ↑(GeometricRealization (oldMesh J N).Vertex (oldMesh J N).triangles)) (y : ↑(GeometricRealization (newMesh J N).Vertex (newMesh J N).triangles)) : (oldMesh J N).coordinateEmbed x = (newMesh J N).coordinateEmbed y ↔ ↑x = ↑y

The two restrictions use the same ambient arrangement vertices, so equality in the plane is exactly equality of their zero-extended barycentric coordinate functions.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.oldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : ↑(GeometricRealization (oldMesh J N).Vertex (oldMesh J N).triangles) → S

Transport the selected polygonal member of an arbitrary synchronized weld to the surface.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : ↑(GeometricRealization (newMesh J N).Vertex (newMesh J N).triangles) → S

Transport the prescribed target member of an arbitrary synchronized weld to the surface.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.isEmbedding_oldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : Topology.IsEmbedding (oldSurfaceEmbed c J N hmodel)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.isEmbedding_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Topology.IsEmbedding (newSurfaceEmbed c J N harr hmodel)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.range_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Set.range (newSurfaceEmbed c J N harr hmodel) = Subtype.val '' ⇑c.chart.symm '' {p : ↑c.kind.modelRegion | ↑p ∈ N.toPlaneComplex.support}

The target surface embedding has exactly the chart image of the prescribed mesh support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.modelInterior_subset_interior_range_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Subtype.val '' ⇑c.chart.symm '' interior {p : ↑c.kind.modelRegion | ↑p ∈ N.toPlaneComplex.support} ⊆ interior (Set.range (newSurfaceEmbed c J N harr hmodel))

Relative interior of the target mesh in the chart model maps to ambient interior in the surface. For half-disk charts this includes points on the model boundary line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.surfaceEmbed_eq_iff {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hold : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) (hnew : N.toPlaneComplex.support ⊆ c.kind.modelRegion) (x : ↑(GeometricRealization (oldMesh J N).Vertex (oldMesh J N).triangles)) (y : ↑(GeometricRealization (newMesh J N).Vertex (newMesh J N).triangles)) : oldSurfaceEmbed c J N hold x = newSurfaceEmbed c J N harr hnew y ↔ ↑x = ↑y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.SynchronizedTarget.exists_local_weld {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hold : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) (hnew : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ ∀ e ∈ (F₁ ∪ F₂).biUnion fun (t : Finset V) => Finset.powersetCard 2 t, {t ∈ F₁ ∪ F₂ | e ⊆ t}.card ≤ 2

Generic finite synchronized weld for a polygonal old-side family and any prescribed finite target mesh lying in the chart model.

A synchronized weld retaining additional certificate lines

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldMesh {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

The selected polygonal side of the common arrangement after finitely many additional certificate cuts.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newMesh {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

The target side of the same additionally cut arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldMesh_support {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : (oldMesh J N lines).toPlaneComplex.support = PolygonalFamily.closedRegion J

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newMesh_support {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (hN : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) : (newMesh J N lines).toPlaneComplex.support = N.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.meshes_triangle_card {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (t : Finset (oldMesh J N lines).Vertex) : t ∈ (oldMesh J N lines).triangles ∪ (newMesh J N lines).triangles → t.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.meshes_surface_edge_valence {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (e : Finset (oldMesh J N lines).Vertex) : (e ∈ ((oldMesh J N lines).triangles ∪ (newMesh J N lines).triangles).biUnion fun (t : Finset (oldMesh J N lines).Vertex) => Finset.powersetCard 2 t) → {t ∈ (oldMesh J N lines).triangles ∪ (newMesh J N lines).triangles | e ⊆ t}.card ≤ 2

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldFaceToAmbient {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleFamily.Face (oldMesh J N lines).triangles → TriangleFamily.Face (PolygonalFamily.relativeSynchronizedArrangement J N lines).triangles

Regard a retained old-side chamber as a chamber of the common ambient arrangement.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldFaceToAmbient J N lines f = ⟨↑f, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newFaceToAmbient {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleFamily.Face (newMesh J N lines).triangles → TriangleFamily.Face (PolygonalFamily.relativeSynchronizedArrangement J N lines).triangles

Regard a retained target-side chamber as a chamber of the common ambient arrangement.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newFaceToAmbient J N lines f = ⟨↑f, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldFaceToAmbient_val {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (f : TriangleFamily.Face (oldMesh J N lines).triangles) : ↑(oldFaceToAmbient J N lines f) = ↑f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newFaceToAmbient_val {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (f : TriangleFamily.Face (newMesh J N lines).triangles) : ↑(newFaceToAmbient J N lines f) = ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.hasCrossEdge_of_ambientAdjacent {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (fOld : TriangleFamily.Face (oldMesh J N lines).triangles) (fNew : TriangleFamily.Face (newMesh J N lines).triangles) (hadj : TriangleFamily.FaceAdjacent (PolygonalFamily.relativeSynchronizedArrangement J N lines).triangles (oldFaceToAmbient J N lines fOld) (newFaceToAmbient J N lines fNew)) : TriangleFamily.HasCrossEdge (oldMesh J N lines).triangles (newMesh J N lines).triangles

Ambient-adjacent chambers retained on opposite sides give a genuine cross-edge certificate for the two synchronized submeshes.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.hasCrossEdge_of_common_triangle {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) {t : Finset (oldMesh J N lines).Vertex} (hOld : t ∈ (oldMesh J N lines).triangles) (hNew : t ∈ (newMesh J N lines).triangles) : TriangleFamily.HasCrossEdge (oldMesh J N lines).triangles (newMesh J N lines).triangles

A chamber retained by both synchronized submeshes supplies a cross-edge certificate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.meshes_coordinateEmbed_eq_iff {ι : Type u_2} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (x : ↑(GeometricRealization (oldMesh J N lines).Vertex (oldMesh J N lines).triangles)) (y : ↑(GeometricRealization (newMesh J N lines).Vertex (newMesh J N lines).triangles)) : (oldMesh J N lines).coordinateEmbed x = (newMesh J N lines).coordinateEmbed y ↔ ↑x = ↑y

Both relative members retain the vertex type of their one ambient arrangement, so planar equality is precisely equality of zero-extended barycentric coordinates.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.oldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : ↑(GeometricRealization (oldMesh J N lines).Vertex (oldMesh J N lines).triangles) → S

The oldSurfaceEmbed declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : ↑(GeometricRealization (newMesh J N lines).Vertex (newMesh J N lines).triangles) → S

The newSurfaceEmbed declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.isEmbedding_oldSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (hmodel : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) : Topology.IsEmbedding (oldSurfaceEmbed c J N lines hmodel)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.isEmbedding_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Topology.IsEmbedding (newSurfaceEmbed c J N lines harr hmodel)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.range_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Set.range (newSurfaceEmbed c J N lines harr hmodel) = Subtype.val '' ⇑c.chart.symm '' {p : ↑c.kind.modelRegion | ↑p ∈ N.toPlaneComplex.support}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.modelInterior_subset_interior_range_newSurfaceEmbed {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hmodel : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : Subtype.val '' ⇑c.chart.symm '' interior {p : ↑c.kind.modelRegion | ↑p ∈ N.toPlaneComplex.support} ⊆ interior (Set.range (newSurfaceEmbed c J N lines harr hmodel))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.RelativeSynchronizedTarget.surfaceEmbed_eq_iff {ι : Type u_2} [Fintype ι] {S : Type u_3} [TopologicalSpace S] (c : MoiseChart S) (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh J).toPlaneComplex.support) (hold : PolygonalFamily.closedRegion J ⊆ c.kind.modelRegion) (hnew : N.toPlaneComplex.support ⊆ c.kind.modelRegion) (x : ↑(GeometricRealization (oldMesh J N lines).Vertex (oldMesh J N lines).triangles)) (y : ↑(GeometricRealization (newMesh J N lines).Vertex (newMesh J N lines).triangles)) : oldSurfaceEmbed c J N lines hold x = newSurfaceEmbed c J N lines harr hnew y ↔ ↑x = ↑y

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacePolygonMeeting {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : A.TileFacesMeeting C hC → PolygonalCircle

The polygonal family obtained by closing the faces meeting an arbitrary compact coordinate set under their whole adaptive source tiles.

Equations

• A.tileFacePolygonMeeting C hC f = Q.facePolygon ↑f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingCertificate {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (f : A.TileFacesMeeting C hC) : FinitePLHomeomorphBetween (Q.faceFillingMap ↑f) LocallyFiniteTriangleComplex.standardFaceRegion (A.tileFacePolygonMeeting C hC f).closedRegion

The retained finite PL filling certificate for one face in a compactly selected whole-tile family.

Equations

• A.tileFaceMeetingCertificate C hC f = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingPullback {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (f : A.TileFacesMeeting C hC) : (A.tileFaceMeetingCertificate C hC f).PullbackSubdivision (SynchronizedPatch.singlePolygonMesh (A.tileFacePolygonMeeting C hC) N f).toPlaneComplex

Pull the synchronized mesh of one compactly selected polygon back to its standard source triangle. The common target refinement includes both the synchronized chart mesh and the retained PL certificate, so the certified inverse is affine on every resulting source piece.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingCertificateLines {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : List (Plane →ᵃ[ℝ] ℝ)

All target-side coordinate lines required by the retained PL certificates of the finite selected face family. Cutting the synchronized arrangement by this one finite list makes every selected chamber subordinate to every certificate whose polygon contains its interior.

Equations

• A.tileFaceMeetingCertificateLines C hC N = List.flatMap (fun (f : A.TileFacesMeeting C hC) => (A.tileFaceMeetingPullback C hC N f).target.toTriangleMesh.coordinateLines) Finset.univ.toList

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingPullback_coordinateLine_mem {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (f : A.TileFacesMeeting C hC) {a : Plane →ᵃ[ℝ] ℝ} (ha : a ∈ (A.tileFaceMeetingPullback C hC N f).target.toTriangleMesh.coordinateLines) : a ∈ A.tileFaceMeetingCertificateLines C hC N

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingLines {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : List (Plane →ᵃ[ℝ] ℝ)

The retained certificate lines together with any additional finite conforming cuts.

Equations

• A.tileFaceMeetingLines C hC N extraLines = A.tileFaceMeetingCertificateLines C hC N ++ extraLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFaceMeetingPullback_coordinateLine_mem_lines {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (f : A.TileFacesMeeting C hC) {a : Plane →ᵃ[ℝ] ℝ} (ha : a ∈ (A.tileFaceMeetingPullback C hC N f).target.toTriangleMesh.coordinateLines) : a ∈ A.tileFaceMeetingLines C hC N extraLines

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.coordinateAnchorLines {α : Type u_2} [Fintype α] (p : α → Plane) : List (Plane →ᵃ[ℝ] ℝ)

Two transverse coordinate cuts through each point in a finite family.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.verticalLine_mem_coordinateAnchorLines {α : Type u_2} [Fintype α] (p : α → Plane) (a : α) : BrokenLineData.verticalLine (p a) ∈ coordinateAnchorLines p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.horizontalLine_mem_coordinateAnchorLines {α : Type u_2} [Fintype α] (p : α → Plane) (a : α) : BrokenLineData.horizontalLine (p a) ∈ coordinateAnchorLines p

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeOldMesh {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

The certificate-cut synchronized old mesh over the finite selected source family.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeNewMesh {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

The target member of the same certificate-cut synchronized arrangement.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeOldMesh_support {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).toPlaneComplex.support = PolygonalFamily.closedRegion (A.tileFacePolygonMeeting C hC)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeNewMesh_support {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (hN : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh (A.tileFacePolygonMeeting C hC)).toPlaneComplex.support) : (A.tileFacesMeetingRelativeNewMesh C hC N extraLines).toPlaneComplex.support = N.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.exists_pullbackTargetTriangle_of_relativeOldTriangle {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (f : A.TileFacesMeeting C hC) {t : Finset (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex} (ht : t ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles) (htf : interior ((PolygonalFamily.relativeSynchronizedArrangement (A.tileFacePolygonMeeting C hC) N (A.tileFaceMeetingLines C hC N extraLines)).triangleCarrier t) ⊆ (A.tileFacePolygonMeeting C hC f).interiorRegion) : ∃ u ∈ (A.tileFaceMeetingPullback C hC N f).target.toTriangleMesh.triangles, (PolygonalFamily.relativeSynchronizedArrangement (A.tileFacePolygonMeeting C hC) N (A.tileFaceMeetingLines C hC N extraLines)).triangleCarrier t ⊆ (A.tileFaceMeetingPullback C hC N f).target.toTriangleMesh.triangleCarrier u

A relative synchronized chamber lying in one selected polygon is contained in a maximal target triangle of that face's retained pullback certificate. This is the precise payoff of putting every certificate coordinate line into the one common arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacePolygonMeeting_closedRegion_subset_region {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : PolygonalFamily.closedRegion (A.tileFacePolygonMeeting C hC) ⊆ V

The compactly selected polygonal union remains in the coordinate region of the replacement presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacePolygonMeeting_subset_complex_support {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : {x : ↑V | ↑x ∈ PolygonalFamily.closedRegion (A.tileFacePolygonMeeting C hC)} ⊆ Q.complex.support

The same polygonal union, lifted to the coordinate-region subtype, lies in the support of the global polygonal replacement complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourceTileFacesMeeting_eq_coordinatePreimage {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) : ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f = {x : K.realization | ∃ (hx : x ∈ U), ↑↑(Q.sourceHomeomorph ⟨x, hx⟩) ∈ PolygonalFamily.closedRegion (A.tileFacePolygonMeeting C hC)}

The coordinate union of a compactly selected tile family is exactly the image of its common-level source subcomplex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeOldCoordinateSupport {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles) → ↑Q.complex.support

The certificate-cut synchronized old mesh, regarded as a subspace of the global replacement support.

Equations

• A.tileFacesMeetingRelativeOldCoordinateSupport C hC N extraLines x = ⟨⟨(A.tileFacesMeetingRelativeOldMesh C hC N extraLines).coordinateEmbed x, ⋯⟩, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isEmbedding_tileFacesMeetingRelativeOldCoordinateSupport {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : Topology.IsEmbedding (A.tileFacesMeetingRelativeOldCoordinateSupport C hC N extraLines)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles) → K.realization

Pull the certificate-cut old coordinate triangulation back through the retained source homeomorphism.

Equations

• A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines = Subtype.val ∘ ⇑Q.sourceHomeomorph.symm ∘ A.tileFacesMeetingRelativeOldCoordinateSupport C hC N extraLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isEmbedding_tileFacesMeetingRelativeSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : Topology.IsEmbedding (A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceEmbed_eq_of_coordinateEmbed_eq {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) {extraLines₁ extraLines₂ : List (Plane →ᵃ[ℝ] ℝ)} (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₁).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₁).triangles)) (y : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₂).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₂).triangles)) (hxy : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₁).coordinateEmbed x = (A.tileFacesMeetingRelativeOldMesh C hC N extraLines₂).coordinateEmbed y) : A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines₁ x = A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines₂ y

Changing only the finite line refinement does not change the source point represented by one fixed planar coordinate.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceComplex {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : IntrinsicTwoComplex

The intrinsic finite complex underlying the certificate-cut selected source mesh.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceComplex_faces {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : (A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).faces = (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceVertexPoint {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (v : (A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).UsedVertex) : K.realization

The original intrinsic point represented by one used vertex of the certificate-cut local source mesh.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceVertexPointInOpen {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (v : (A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).UsedVertex) : ↑U

The same local source vertex, retaining its proof of membership in the replacement domain.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceVertexPointInOpen_val {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (v : (A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).UsedVertex) : ↑(A.tileFacesMeetingRelativeSourceVertexPointInOpen C hC N extraLines v) = A.tileFacesMeetingRelativeSourceVertexPoint C hC N extraLines v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourceHomeomorph_relativeSourceVertexPointInOpen {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (v : (A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).UsedVertex) : ↑↑(Q.sourceHomeomorph (A.tileFacesMeetingRelativeSourceVertexPointInOpen C hC N extraLines v)) = (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).position ↑v

In replacement coordinates, a used local source vertex is its literal plane-mesh vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.injective_tileFacesMeetingRelativeSourceVertexPoint {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : Function.Injective (A.tileFacesMeetingRelativeSourceVertexPoint C hC N extraLines)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.range_tileFacesMeetingRelativeSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : Set.range (A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines) = ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f

The certificate cuts change only the triangulation, not the selected whole-tile source support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.range_tileFacesMeetingRelativeSourceEmbed_eq_levelFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) : Set.range (A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines) = ⋃ (u : ↥(A.levelFaces (A.tilesMeeting C hC))), K.levelFaceCarrier ↑u

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingRelativeSourceEmbed_affineOn_triangle {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) {t : Finset (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex} (ht : t ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles) : ∃ (a : ((A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ), ∀ (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)), (∀ v ∉ t, ↑x v = 0) → ↑(A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines x) = a ↑x

On every certificate-cut synchronized triangle, the pulled-back source embedding is one affine function in the original intrinsic barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.exists_parentFace_of_relativeOldTriangle {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) {t : Finset (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex} (ht : t ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles) : ∃ (u : K.Face), ∀ (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)), (∀ v ∉ t, ↑x v = 0) → A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines x ∈ K.faceCarrier ↑u

Every relative source triangle lies in one original maximal face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParent {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : K.Face

A canonical original parent face for one triangle of the relative source mesh.

Equations

• A.relativeOldTriangleParent C hC N extraLines t = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParent_contains {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)) (hx : ∀ v ∉ ↑t, ↑x v = 0) : A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines x ∈ K.faceCarrier ↑(A.relativeOldTriangleParent C hC N extraLines t)

The chosen parent contains the complete image of the relative source triangle.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleSourceAffine {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : ((A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

The canonical affine formula for the source embedding on one relative triangle.

Equations

• A.relativeOldTriangleSourceAffine C hC N extraLines t = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleSourceAffine_eq {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)) (hx : ∀ v ∉ ↑t, ↑x v = 0) : ↑(A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines x) = (A.relativeOldTriangleSourceAffine C hC N extraLines t) ↑x

The chosen source affine formula agrees with the source embedding on its triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeSourceFaceMap_eq_vertex_sum {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (x : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)) (hx : ∀ v ∉ ↑t, ↑x v = 0) : ↑(A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines x) = ∑ v : ↥↑t, ↑x ↑v • ↑(A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines ((A.tileFacesMeetingRelativeSourceComplex C hC N extraLines).vertexPoint ⟨↑v, ⋯⟩))

On one relative source triangle, the source map is the affine combination of its three actual source-vertex images.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleAsPlaneTriangle {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).toPlaneComplex.toTriangleMesh.Triangle

The same abstract triangle, viewed as a maximal triangle of the plane complex generated by the relative mesh.

Equations

• A.relativeOldTriangleAsPlaneTriangle C hC N extraLines t = ⟨↑t, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTrianglePoint {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (p : { p : Plane // p ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t }) : ↑(GeometricRealization (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangles)

A point of a relative old plane triangle, regarded as the corresponding point of its barycentric realization.

Equations

• A.relativeOldTrianglePoint C hC N extraLines t p = ⟨((A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCoords t) ↑p, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTrianglePoint_coordinateEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (p : { p : Plane // p ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t }) : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).coordinateEmbed (A.relativeOldTrianglePoint C hC N extraLines t p) = ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTrianglePoint_val_eq_triangleCoords {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (p : { p : Plane // p ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t }) : ↑(A.relativeOldTrianglePoint C hC N extraLines t p) = ((A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCoords t) ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTrianglePoint_supported {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (p : { p : Plane // p ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t }) (v : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Vertex) : v ∉ ↑t → ↑(A.relativeOldTrianglePoint C hC N extraLines t p) v = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParentPlaneAffine {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : Plane →ᵃ[ℝ] Plane

The source triangle written in the standard plane coordinates of its original parent face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParentPlaneAffine_eq {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) (p : { p : Plane // p ∈ (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t }) : (A.relativeOldTriangleParentPlaneAffine C hC N extraLines t) ↑p = ↑((K.facePlaneHomeomorph (A.relativeOldTriangleParent C hC N extraLines t)) ⟨A.tileFacesMeetingRelativeSourceEmbed C hC N extraLines (A.relativeOldTrianglePoint C hC N extraLines t p), ⋯⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParentPlaneAffine_injOn {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : Set.InjOn (⇑(A.relativeOldTriangleParentPlaneAffine C hC N extraLines t)) ((A.tileFacesMeetingRelativeOldMesh C hC N extraLines).triangleCarrier ↑t)

The parent-plane formula is locally injective on its source triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParentPlaneAffine_injective {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : Function.Injective ⇑(A.relativeOldTriangleParentPlaneAffine C hC N extraLines t)

Consequently, the parent-plane formula is a global affine equivalence at the level of functions.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeOldTriangleParentPlaneAffine_surjective {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (extraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N extraLines).Triangle) : Function.Surjective ⇑(A.relativeOldTriangleParentPlaneAffine C hC N extraLines t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParent (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : K.Face

A canonical original parent of one face at a fixed midpoint level.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParent K s = ⟨Classical.choose ⋯, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParent_contains (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (x : (K.safeSubdivision n).refined.realization) (hx : x ∈ (K.safeSubdivision n).refined.faceCarrier ↑s) : (K.safeSubdivision n).homeo x ∈ K.faceCarrier ↑(levelFaceParent K s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceSourceAffine (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : ((K.safeSubdivision n).refined.Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

The canonical affine formula of the midpoint-subdivision homeomorphism on one level face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceSourceAffine K s = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceSourceAffine_eq (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (x : (K.safeSubdivision n).refined.realization) (hx : x ∈ (K.safeSubdivision n).refined.faceCarrier ↑s) : ↑((K.safeSubdivision n).homeo x) = (levelFaceSourceAffine K s) ↑x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentPlaneAffine (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : Plane →ᵃ[ℝ] Plane

A level face, transported to the standard plane chart of its original parent, is affine in its own standard triangle coordinates.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentPlaneAffine_eq (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (p : ↑standardTrianglePlaneComplex.support) : (levelFaceParentPlaneAffine K s) ↑p = ↑((K.facePlaneHomeomorph (levelFaceParent K s)) ⟨(K.safeSubdivision n).homeo ↑(((K.safeSubdivision n).refined.facePlaneHomeomorph s).symm p), ⋯⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentPlaneAffine_injOn (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : Set.InjOn (⇑(levelFaceParentPlaneAffine K s)) standardTrianglePlaneComplex.support

The parent-plane formula for a level face is injective on the standard closed triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentPlaneAffine_injective (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : Function.Injective ⇑(levelFaceParentPlaneAffine K s)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentPlaneAffine_surjective (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) : Function.Surjective ⇑(levelFaceParentPlaneAffine K s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentCoord (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (k : Fin 3) : Plane →ᵃ[ℝ] ℝ

Barycentric coordinate of a level face after transport to its original parent plane.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentCoord_vertex (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (k i : Fin 3) : (levelFaceParentCoord K s k) ((levelFaceParentPlaneAffine K s) (standardTriangleVertex i)) = if k = i then 1 else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentCoord_surjective (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (k : Fin 3) : Function.Surjective ⇑(levelFaceParentCoord K s k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.levelFaceParentCoord_nonneg (K : IntrinsicTwoComplex) {n : ℕ} (s : K.LevelFace n) (k : Fin 3) (p : ↑standardTrianglePlaneComplex.support) : 0 ≤ (levelFaceParentCoord K s k) ((levelFaceParentPlaneAffine K s) ↑p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.face_eq_of_mem_faceCarriers_of_facePlane_mem_interior (K : IntrinsicTwoComplex) (t u : K.Face) (x : K.realization) (hxt : x ∈ K.faceCarrier ↑t) (hxu : x ∈ K.faceCarrier ↑u) (hxint : ↑((K.facePlaneHomeomorph t) ⟨x, hxt⟩) ∈ interior standardTrianglePlaneComplex.support) : t = u

A point in the relative interior of an original maximal face cannot also belong to a distinct original maximal face. The relative interior is detected in the canonical standard plane chart.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeLevelAlignmentLines {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (baseExtraLines : List (Plane →ᵃ[ℝ] ℝ)) (n : ℕ) : List (Plane →ᵃ[ℝ] ℝ)

Pull every fixed-level face coordinate back through every relative source triangle whose chosen original parent agrees. Cutting by these finitely many affine lines makes the next relative source mesh subordinate to the fixed-level triangulation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeLevelAlignmentLine_mem {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (baseExtraLines : List (Plane →ᵃ[ℝ] ℝ)) (n : ℕ) (t : (A.tileFacesMeetingRelativeOldMesh C hC N baseExtraLines).Triangle) (s : K.LevelFace n) (hparent : levelFaceParent K s = A.relativeOldTriangleParent C hC N baseExtraLines t) (k : Fin 3) : (levelFaceParentCoord K s k).comp (A.relativeOldTriangleParentPlaneAffine C hC N baseExtraLines t) ∈ A.relativeLevelAlignmentLines C hC N baseExtraLines n

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.relativeLevelAlignmentLine_surjective {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) (baseExtraLines : List (Plane →ᵃ[ℝ] ℝ)) (t : (A.tileFacesMeetingRelativeOldMesh C hC N baseExtraLines).Triangle) {n : ℕ} (s : K.LevelFace n) (k : Fin 3) : Function.Surjective ⇑((levelFaceParentCoord K s k).comp (A.relativeOldTriangleParentPlaneAffine C hC N baseExtraLines t))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingOldCoordinateSupport {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : ↑(GeometricRealization (SynchronizedTarget.oldMesh (A.tileFacePolygonMeeting C hC) N).Vertex (SynchronizedTarget.oldMesh (A.tileFacePolygonMeeting C hC) N).triangles) → ↑Q.complex.support

The synchronized old coordinate mesh, regarded as a subspace of the global replacement support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isEmbedding_tileFacesMeetingOldCoordinateSupport {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : Topology.IsEmbedding (A.tileFacesMeetingOldCoordinateSupport C hC N)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacesMeetingSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : ↑(GeometricRealization (SynchronizedTarget.oldMesh (A.tileFacePolygonMeeting C hC) N).Vertex (SynchronizedTarget.oldMesh (A.tileFacePolygonMeeting C hC) N).triangles) → K.realization

Pull the synchronized old coordinate triangulation back through the retained source homeomorphism to the original finite intrinsic realization.

Equations

• A.tileFacesMeetingSourceEmbed C hC N = Subtype.val ∘ ⇑Q.sourceHomeomorph.symm ∘ A.tileFacesMeetingOldCoordinateSupport C hC N

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.isEmbedding_tileFacesMeetingSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : Topology.IsEmbedding (A.tileFacesMeetingSourceEmbed C hC N)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.range_tileFacesMeetingSourceEmbed {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : Set.range (A.tileFacesMeetingSourceEmbed C hC N) = ⋃ (f : A.TileFacesMeeting C hC), Q.sourceFaceSet ↑f

The synchronized old mesh pulls back onto exactly the finite whole-tile source subcomplex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.range_tileFacesMeetingSourceEmbed_eq_levelFaces {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (N : TriangleMesh) : Set.range (A.tileFacesMeetingSourceEmbed C hC N) = ⋃ (u : ↥(A.levelFaces (A.tilesMeeting C hC))), K.levelFaceCarrier ↑u

In intrinsic terms, the range is a literal subcomplex of one finite midpoint level.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.tileFacePolygonMeeting_closedRegion_subset_modelRegion {S : Type u_2} [TopologicalSpace S] {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} (c : MoiseChart S) {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (g' : ↑U → ↑c.kind.modelRegion) (hcoord : ∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : PolygonalFamily.closedRegion (A.tileFacePolygonMeeting C hC) ⊆ c.kind.modelRegion

Every polygon in a compactly selected tile family lies in the chart model whenever the retained coordinate homeomorphism does.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.exists_tileFacesMeeting_local_weld {S : Type u_2} [TopologicalSpace S] {K : IntrinsicTwoComplex} {U : Set K.realization} {V : Set Plane} (c : MoiseChart S) {Q : PolygonalReplacementPresentation (↑U) V} (A : PolygonalReplacementSourceAtlas K U V Q) (C : Set ↑V) (hC : IsCompact C) (g' : ↑U → ↑c.kind.modelRegion) (hcoord : ∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) (N : TriangleMesh) (harr : N.toPlaneComplex.support ⊆ (PolygonalFamily.arrangementMesh (A.tileFacePolygonMeeting C hC)).toPlaneComplex.support) (hnew : N.toPlaneComplex.support ⊆ c.kind.modelRegion) : ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (F₁ : Finset (Finset W)) (F₂ : Finset (Finset W)) (e₁ : ↑(GeometricRealization W F₁) → S) (e₂ : ↑(GeometricRealization W F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization W F₁)) (y : ↑(GeometricRealization W F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization W F₁)) (y : ↑(GeometricRealization W F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ ∀ e ∈ (F₁ ∪ F₂).biUnion fun (t : Finset W) => Finset.powersetCard 2 t, {t ∈ F₁ ∪ F₂ | e ⊆ t}.card ≤ 2

A compactly selected whole-tile family admits a synchronized local weld with any prescribed finite target mesh in the same chart model.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTileFacePolygon {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : A.PatchTileFaces → PolygonalCircle

The polygonal family obtained by retaining every fan face in every adaptive tile touched by the patch.

Equations

• A.patchTileFacePolygon f = Q.facePolygon ↑f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTileFaceCertificate {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (f : A.PatchTileFaces) : FinitePLHomeomorphBetween (Q.faceFillingMap ↑f) LocallyFiniteTriangleComplex.standardFaceRegion (A.patchTileFacePolygon f).closedRegion

The retained finite PL certificate for one face of the tile-closed source family.

Equations

• A.patchTileFaceCertificate f = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTileFacePullback {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (N : TriangleMesh) (f : A.PatchTileFaces) : (A.patchTileFaceCertificate f).PullbackSubdivision (SynchronizedPatch.singlePolygonMesh A.patchTileFacePolygon N f).toPlaneComplex

Pull the synchronized mesh of one selected polygon back to its standard source triangle. The target side is first commonly refined with the original Schoenflies certificate, so the result carries every chart-patch intersection vertex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.sourcePatchTileFaces_eq_coordinatePreimage {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) : ⋃ (f : A.PatchTileFaces), Q.sourceFaceSet ↑f = {x : K.realization | ∃ (hx : x ∈ U), ↑↑(Q.sourceHomeomorph ⟨x, hx⟩) ∈ PolygonalFamily.closedRegion A.patchTileFacePolygon}

The exact coordinate union of the tile-closed family is the image, under the retained source homeomorphism, of its exact common-level source subcomplex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.patchTileFaceClosedRegion_subset_modelRegion {K : IntrinsicTwoComplex} {U : Set K.realization} {k : ChartKind} {Q : PolygonalReplacementPresentation (↑U) k.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U k.perturbationRegion Q) (g' : ↑U → ↑k.modelRegion) (hcoord : ∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : PolygonalFamily.closedRegion A.patchTileFacePolygon ⊆ k.modelRegion

Every polygon in the tile-closed family still lies in the chart model (including the half-plane condition in the bordered case).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.PolygonalReplacementSourceAtlas.exists_patchTile_local_weld {S : Type u_2} [TopologicalSpace S] {K : IntrinsicTwoComplex} {U : Set K.realization} (c : MoiseChart S) {Q : PolygonalReplacementPresentation (↑U) c.kind.perturbationRegion} (A : PolygonalReplacementSourceAtlas K U c.kind.perturbationRegion Q) (g' : ↑U → ↑c.kind.modelRegion) (hcoord : ∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ ∀ e ∈ (F₁ ∪ F₂).biUnion fun (t : Finset V) => Finset.powersetCard 2 t, {t ∈ F₁ ∪ F₂ | e ⊆ t}.card ≤ 2

The corrected finite local weld: its old side is closed under whole adaptive source tiles, so it is exactly supported on a finite common-level source subcomplex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_straightenedChartOpen {S' : Type u_2} [TopologicalSpace S'] [T2Space S'] [CompactSpace S'] [SecondCountableTopology S'] [ChartedSpace (EuclideanHalfSpace 2) S'] (T : PartialTriangulation S') (c : MoiseChart S') (hc : c.BoundaryFaithful) (hboundary : T.BoundaryFacewiseRegular) (U : Set T.toIntrinsic.realization) (hU : IsOpen U) (hsub : U ⊆ T.chartOverlap c) (V : Set Plane) (hV : IsOpen V) (hVsub : V ⊆ c.kind.perturbationRegion) (hmem : ∀ (x : ↑U), T.chartOverlapMap c ⟨↑x, ⋯⟩ ∈ V) (hfVclosed : Topology.IsClosedEmbedding fun (x : ↑U) => ⟨T.chartOverlapMap c ⟨↑x, ⋯⟩, ⋯⟩) : ∃ (Q : PolygonalReplacementPresentation (↑U) V) (x : PolygonalReplacementSourceAtlas T.toIntrinsic U V Q) (g' : ↑U → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S'), (∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) ∧ (c.kind = ChartKind.halfDisk → ∀ (y : ↑U), (↑↑(Q.sourceHomeomorph y)).ofLp 0 = 0 ↔ T.embed ↑y ∈ ModelWithCorners.boundary S') ∧ (∀ (y : ↑U), g ↑y = ↑(c.chart.symm (g' y))) ∧ (∀ x ∉ U, g x = T.embed x) ∧ MatchesAtFrontier U g T.embed ∧ ContinuousOn g U ∧ Set.InjOn g U ∧ Disjoint (g '' U) (T.embed '' Uᶜ) ∧ Topology.IsEmbedding (frontierGlue U g T.embed)

Assemble the controlled polygonal replacement over an arbitrary open chart region whose coordinate image is closed relative to the chosen plane perturbation region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_straightenedChartAway {S' : Type u_2} [TopologicalSpace S'] [T2Space S'] [CompactSpace S'] [SecondCountableTopology S'] [ChartedSpace (EuclideanHalfSpace 2) S'] (T : PartialTriangulation S') (c : MoiseChart S') (hc : c.BoundaryFaithful) (hboundary : T.BoundaryFacewiseRegular) (A : Set S') (hA : IsClosed A) : ∃ (U : Set T.toIntrinsic.realization) (_ : IsOpen U) (V : Set Plane) (_ : IsOpen V) (Q : PolygonalReplacementPresentation (↑U) V) (x : PolygonalReplacementSourceAtlas T.toIntrinsic U V Q) (g' : ↑U → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S'), V ⊆ c.kind.perturbationRegion ∧ (∀ (z : ↑c.kind.modelRegion), ↑z ∉ V → ↑(c.chart.symm z) ∈ A) ∧ (∀ (y : ↑(T.chartOverlap c)), T.embed ↑y ∈ A → T.chartOverlapMap c y ∉ V) ∧ (∀ (y : ↑(T.chartOverlap c)), ↑y ∉ U → T.embed ↑y ∈ A) ∧ (∀ (y : ↑U), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) ∧ (c.kind = ChartKind.halfDisk → ∀ (y : ↑U), (↑↑(Q.sourceHomeomorph y)).ofLp 0 = 0 ↔ T.embed ↑y ∈ ModelWithCorners.boundary S') ∧ U ⊆ T.chartOverlap c ∧ (∀ (y : ↑U), g ↑y = ↑(c.chart.symm (g' y))) ∧ (∀ (x : ↑(GeometricRealization T.Vertex T.faces)), T.embed x ∈ A → g x = T.embed x) ∧ MatchesAtFrontier U g T.embed ∧ ContinuousOn g U ∧ Set.InjOn g U ∧ Disjoint (g '' U) (T.embed '' Uᶜ) ∧ Topology.IsEmbedding (frontierGlue U g T.embed)

Straighten the old complex in a chart while fixing every source point whose old image lies in a prescribed closed protected set. The perturbation region is obtained by deleting the protected chart trace; closedness of the full overlap embedding makes the restricted trace closed in that new open region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_glued {S : Type u_1} [TopologicalSpace S] [T2Space S] [ChartedSpace (EuclideanHalfSpace 2) S] (V : Type) [Fintype V] [DecidableEq V] (F₁ F₂ : Finset (Finset V)) (hcard : ∀ t ∈ F₁ ∪ F₂, t.card = 3) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S) (he₁ : Topology.IsEmbedding e₁) (he₂ : Topology.IsEmbedding e₂) (hagree : ∀ (x : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x = ↑y → e₁ x = e₂ y) (hsep : ∀ (x : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x = e₂ y → ↑x = ↑y) (hboundary₁ : BoundaryFacewiseRegularEmbedding F₁ e₁) (hboundary₂ : BoundaryFacewiseRegularEmbedding F₂ e₂) : ∃ (T' : PartialTriangulation S) (vertexEquiv : T'.Vertex ≃ V), relabelFaceFamily vertexEquiv.toEmbedding T'.faces = F₁ ∪ F₂ ∧ T'.support = Set.range e₁ ∪ Set.range e₂ ∧ (∀ e ∈ T'.edges, {t ∈ T'.faces | e ⊆ t}.card ≤ 2) ∧ T'.BoundaryFacewiseRegular

Theorem boundary (Moise Thm. 7.6 for partial triangulations).

Two partial triangulations presented on a common vertex type, whose embeddings agree exactly on the shared part of their realizations (hagree and hsep together say the images meet only where the barycentric points coincide), glue to a single partial triangulation on the union face family, supported on the union of the two images.

The realization of the union family is the set-union of the two realizations, so the glued embedding is the pasting of the two embeddings along a closed common part; it is a continuous injection from a compact space into a Hausdorff space, hence an embedding. The edge-face count hypothesis is passed through to the glued complex. The conclusion retains an equivalence from the glued vertex type to V under which its face family relabels to F₁ ∪ F₂, so later incidence certificates can use the two source-family proofs without reconstructing provenance from the embedding.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isDualConnected_of_faces_eq_union {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) {F₁ F₂ : Finset (Finset T.Vertex)} (hfaces : T.faces = F₁ ∪ F₂) (hdual₁ : TriangleFamily.IsDualConnected F₁) (hdual₂ : TriangleFamily.IsDualConnected F₂) (hcross : TriangleFamily.HasCrossEdge F₁ F₂) : T.IsDualConnected

A glued partial triangulation is dual-connected once both source families are dual-connected and one source face on each side shares an edge in the union family.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.RadoInvariant {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (T : PartialTriangulation S) (A : Set S) : Prop

The invariant carried through the bordered Radó induction: every edge of the built complex lies in at most two faces, every triangle has a regular exposed intersection with the ambient manifold boundary, and the region A absorbed so far lies in the topological interior of its support in S.

For a surface without boundary this agrees with Moise Ch. 8, Thm. 3, invariant (4), after the usual identification of topological and combinatorial interior. The ambient topological interior is essential in the bordered case: a half-disk core contains points of ∂S, and those points belong to the interior of a half-disk neighborhood as a subset of S, although they lie on its combinatorial boundary. Requiring such points to lie in a combinatorial-interior subset would make the bordered induction statement false.

This deliberately does not call the intermediate support a combinatorial manifold: edge valence alone does not imply connected vertex links. The crossing construction needs the stated edge/boundary regularity and exact embedded gluing; after the final support is all of S, the homeomorphism to S supplies the topological surface conclusion directly.

• coresCompact : IsCompact A

  The finitely many absorbed chart cores form a compact set. This is needed to choose the finite collars and positive separation scales in the induction step.

• combSurface (e : Finset T.Vertex) : e ∈ T.edges → {t ∈ T.faces | e ⊆ t}.card ≤ 2
• boundaryFacewiseRegular : T.BoundaryFacewiseRegular

  Every triangle meets the ambient manifold boundary in one exposed simplicial face.

• coresInside : A ⊆ interior T.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.RadoInvariant.coresCovered {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {T : PartialTriangulation S} {A : Set S} (hT : RadoInvariant T A) : A ⊆ T.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.RadoInvariant.exists_closedBuffer {S : Type u_1} [TopologicalSpace S] [T2Space S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {T : PartialTriangulation S} {A : Set S} (hT : RadoInvariant T A) : ∃ (C : Set S), IsClosed C ∧ A ⊆ interior C ∧ C ⊆ interior T.support

The already absorbed compact set has a closed buffer still lying in the ambient interior of the old support. Protecting this whole buffer during chart straightening, rather than merely protecting A pointwise, makes preservation of the Radó interior invariant immediate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.RadoInvariant.absorb_of_subset {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {T : PartialTriangulation S} {A B : Set S} (hT : RadoInvariant T A) (hBcompact : IsCompact B) (hB : B ⊆ interior T.support) : RadoInvariant T (A ∪ B)

Enlarge the recorded absorbed set without changing the triangulation when the added set is already in the interior of its support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.radoInvariant_chartPatch {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (c : MoiseChart S) (hc : c.BoundaryFaithful) : RadoInvariant c.patchPartialTriangulation c.core

A single chart has a concrete finite partial triangulation satisfying the bordered Rado invariant. This is the honest nonempty base patch used by the induction step.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.radoInvariant_chartPatch_absorb {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (c : MoiseChart S) (hc : c.BoundaryFaithful) {A : Set S} (hAcompact : IsCompact A) (hA : A ⊆ interior c.patchPartialTriangulation.support) : RadoInvariant c.patchPartialTriangulation (A ∪ c.core)

If the fixed patch of the new chart already contains the previously absorbed region in its ambient interior, that patch alone is a valid next induction stage.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.radoInvariant_empty (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : RadoInvariant (PartialTriangulation.empty S) ∅

The empty partial triangulation satisfies the invariant for the empty region: the base case of the Radó induction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_finite_chart_open_cover (S : Type u_1) [TopologicalSpace S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : ∃ (m : ℕ) (charts : Fin m → MoiseChart S), ⋃ (i : Fin m), interior (charts i).core = Set.univ ∧ (∀ (i : Fin m), (charts i).BoundaryFaithful) ∧ ∀ (i j : Fin m), Relation.TransGen (fun (a b : Fin m) => (interior (charts a).core ∩ interior (charts b).core).Nonempty) i j

A compact Eval surface has a finite cover by interiors of boundary-faithful Moise chart cores. Because the ambient surface is connected, the graph joining two cores when their interiors overlap is connected as well.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_finite_chart_cover (S : Type u_1) [TopologicalSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : ∃ (m : ℕ) (charts : Fin m → MoiseChart S), ⋃ (i : Fin m), (charts i).core = Set.univ ∧ ∀ (i : Fin m), (charts i).BoundaryFaithful

A compact Eval surface has a finite cover by boundary-faithful Moise chart cores (Moise Ch. 8, Thm. 1, plus compactness). Proved by a finite subcover of the core interiors from the local chart extraction (exists_moiseChart_core_mem_nhds, Moise/ChartExtraction.lean).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_secondCountableTopology (S : Type u_1) [TopologicalSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : SecondCountableTopology S

Compact Eval surfaces are second countable. We derive this from the finite Moise chart cover instead of asking typeclass search to infer second countability of the half-space model: each chart domain is homeomorphic to a second-countable disk or half-disk, and finitely many open chart domains cover the surface.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PreservesManifoldBoundary (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {X : Type u_2} (f g : X → S) : Prop

Two embeddings of the same source preserve the ambient manifold-boundary stratum pointwise. This is the exact relative certificate needed by the crossing weld.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PreservesManifoldBoundary S f g = ∀ (x : X), f x ∈ ModelWithCorners.boundary S ↔ g x ∈ ModelWithCorners.boundary S

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.BoundaryPreservingStraightening (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (T : PartialTriangulation S) (c : MoiseChart S) : Prop

The raw chart straightening, augmented only with the certificate that its frontier-glued embedding preserves ambient boundary membership. The crossing-weld implementation consumes this proposition to retain the boundary-line subcomplex during the bordered induction.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_boundaryPreservingStraightening (S : Type u_1) [TopologicalSpace S] [T2Space S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (T : PartialTriangulation S) (c : MoiseChart S) (hc : c.BoundaryFaithful) (hboundary : T.BoundaryFacewiseRegular) : BoundaryPreservingStraightening S T c

The relative polygonal straightening preserves the ambient boundary stratum.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.exists_straightenedChartOverlap (S : Type u_1) [TopologicalSpace S] [T2Space S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (T : PartialTriangulation S) (c : MoiseChart S) : ∃ (Q : PolygonalReplacementPresentation (↑(T.chartOverlap c)) c.kind.perturbationRegion) (x : PolygonalReplacementSourceAtlas T.toIntrinsic (T.chartOverlap c) c.kind.perturbationRegion Q) (g' : ↑(T.chartOverlap c) → ↑c.kind.modelRegion) (g : T.toIntrinsic.realization → S), (∀ (y : ↑(T.chartOverlap c)), ↑(g' y) = ↑↑(Q.sourceHomeomorph y)) ∧ (∀ (y : ↑(T.chartOverlap c)), g ↑y = ↑(c.chart.symm (g' y))) ∧ MatchesAtFrontier (T.chartOverlap c) g T.embed ∧ ContinuousOn g (T.chartOverlap c) ∧ Set.InjOn g (T.chartOverlap c) ∧ Disjoint (g '' T.chartOverlap c) (T.embed '' (T.chartOverlap c)ᶜ) ∧ Topology.IsEmbedding (frontierGlue (T.chartOverlap c) g T.embed)

The controlled locally finite polygonal replacement on the full chart overlap assembles with the unchanged old embedding across the overlap frontier.

This is the analytic half of Moise's crossing step. The replacement stays in the chart model (including the closed half-plane in the bordered case), converges to the old embedding at the frontier, and is disjoint from the unchanged image outside the overlap. Consequently the frontier paste is again an embedding of the original finite intrinsic complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_positive_weight_on_both_sides_of_gap {ι : Type u_2} [Fintype ι] (weight value : ι → ℝ) (a b z : ℝ) (hweight : ∀ (i : ι), 0 ≤ weight i) (hweightSum : ∑ i : ι, weight i = 1) (hzAverage : z = ∑ i : ι, weight i * value i) (hgap : ∀ (i : ι), 0 < weight i → value i ∉ Set.Ioo a b) (hzGap : z ∈ Set.Ioo a b) : (∃ (i : ι), 0 < weight i ∧ value i ≤ a) ∧ ∃ (i : ι), 0 < weight i ∧ b ≤ value i

If a convex average lies strictly inside a gap avoided by every positively weighted value, then some positive weight occurs on each side of the gap. Keeping this order argument separate prevents the crossing-weld elaborator from repeatedly reducing its large dependent local types.