Cellwise extension of a close intrinsic graph approximation #
This file applies polygonal Schoenflies face by face to the arbitrarily close graph embedding
from IntrinsicCloseGraphApproximation. The proofs parallel the first intrinsic cellwise
construction, but the boundary map is now the second, metrically controlled graph replacement.
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceBoundaryMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
The close graph embedding in standard coordinates on one face boundary.
Equations
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceBoundaryMap_apply
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
(p : StandardFaceBoundary)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.continuousOn_faceBoundaryMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.injOn_faceBoundaryMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceBoundaryMap_isPLOnSet
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.exists_imagePolygon
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
∃ (J : PolygonalCircle), J.carrier = A.faceBoundaryMap t '' frontier standardFaceRegion
The image of a close face-boundary map is a polygonal circle.
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.imagePolygon
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
The polygon which is the exact image of one close face-boundary map.
Equations
- A.imagePolygon t = Classical.choose ⋯
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.imagePolygon_carrier
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
structure
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
A certified PL filling of one close face boundary.
The
mapdeclaration.- eqOn_boundary : Set.EqOn self.map (A.faceBoundaryMap t) (frontier standardFaceRegion)
- continuousOn : ContinuousOn self.map standardFaceRegion
- injectiveOn : Set.InjOn self.map standardFaceRegion
- isPLOnSet : IsPLOnSet standardFaceRegion self.map
- certificate : Nonempty (FinitePLHomeomorphBetween self.map standardFaceRegion (A.imagePolygon t).closedRegion)
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.exists_faceFilling
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
Nonempty (A.FaceFilling t)
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceFilling
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
A.FaceFilling t
The faceFilling declaration.
Equations
- A.faceFilling t = Classical.choice ⋯
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling.faceInteriorMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t : K.Face}
(F : A.FaceFilling t)
:
K.ClosedFace t → Plane
The faceInteriorMap declaration.
Equations
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling.continuous_intrinsicMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t : K.Face}
(F : A.FaceFilling t)
:
Continuous (faceInteriorMap A F)
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling.injective_intrinsicMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t : K.Face}
(F : A.FaceFilling t)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling.range_intrinsicMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t : K.Face}
(F : A.FaceFilling t)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.FaceFilling.mapsTo_interiorRegion
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t : K.Face}
(F : A.FaceFilling t)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceFilling_eq_of_boundaryLift_eq
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{t u : K.Face}
{p q : StandardFaceBoundary}
(hpq : ↑(faceBoundaryLift t p) = ↑(faceBoundaryLift u q))
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.faceFilling_intrinsicMap_eq
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t u : K.Face)
{x : K.realization}
(hxt : x ∈ K.faceCarrier ↑t)
(hxu : x ∈ K.faceCarrier ↑u)
:
FaceFilling.faceInteriorMap A (A.faceFilling t) ⟨x, hxt⟩ = FaceFilling.faceInteriorMap A (A.faceFilling u) ⟨x, hxu⟩
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.closeCellwiseMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(x : K.realization)
:
The finite family of close face fillings, glued on the canonical realization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.closeCellwiseMap_eqOn_face
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
(x : K.realization)
(hxt : x ∈ K.faceCarrier ↑t)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.continuous_closeCellwiseMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.closeCellwiseMap_eq_intrinsicMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{x : K.realization}
(hx : x ∈ K.oneSkeleton)
:
def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.VerticesAvoidClosedRegions
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
:
The approximated graph avoids the selected closed region of every nonincident face at all outside vertices.
Equations
- A.VerticesAvoidClosedRegions = ∀ (t : K.Face) (v : K.UsedVertex), ↑v ∉ ↑t → A.intrinsicMap (K.vertexPoint v) ∉ (A.imagePolygon t).closedRegion
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.verticesAvoidClosedRegions_of_close
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{r : ℝ}
(hr : 0 < r)
(hsep :
∀ (t : K.Face) (v : K.UsedVertex),
↑v ∉ ↑t → Disjoint (Metric.closedBall (h (K.vertexPoint v)) r) (Metric.cthickening r (h '' K.faceCarrier ↑t)))
(hclose : ∀ x ∈ K.oneSkeleton, dist (A.intrinsicMap x) (h x) < r)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.imagePolygon_carrier_subset_graph
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
:
(A.imagePolygon t).carrier ⊆ A.intrinsicMap '' K.oneSkeleton
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.mem_faceCarrier_of_intrinsicMap_mem_imagePolygon
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
{x : K.realization}
(hx : x ∈ K.oneSkeleton)
(himage : A.intrinsicMap x ∈ (A.imagePolygon t).carrier)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.intrinsicMap_mem_imagePolygon
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(t : K.Face)
{x : K.realization}
(hxt : x ∈ K.faceCarrier ↑t)
(hx : x ∈ K.oneSkeleton)
:
def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.GraphAvoidsInteriors
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
:
The global close graph avoids the bounded interior selected for every filled face.
Equations
- A.GraphAvoidsInteriors = ∀ (t : K.Face), Disjoint (A.intrinsicMap '' K.oneSkeleton) (A.imagePolygon t).interiorRegion
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.vertex_mem_exterior
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hvertices : A.VerticesAvoidClosedRegions)
(t : K.Face)
(v : K.UsedVertex)
(hvt : ↑v ∉ ↑t)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.graphAvoidsInteriors_of_verticesAvoid
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hvertices : A.VerticesAvoidClosedRegions)
:
The endpoint exterior condition propagates along each connected intrinsic edge, so the whole close graph avoids every nonincident bounded face interior.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.closeCellwiseMap_dist_le
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
{η ρ : ℝ}
(hsmall : ∀ (t : K.Face), ∀ x ∈ K.faceCarrier ↑t, ∀ y ∈ K.faceCarrier ↑t, dist (h x) (h y) < η)
(hclose : ∀ x ∈ K.oneSkeleton, dist (A.intrinsicMap x) (h x) < ρ)
(x : K.realization)
:
Quantitative control of the close cellwise filling.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.disjoint_imagePolygon_interiors
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hside : A.GraphAvoidsInteriors)
(t u : K.Face)
(htu : t ≠ u)
:
Disjoint (A.imagePolygon t).interiorRegion (A.imagePolygon u).interiorRegion
Distinct face polygons have disjoint bounded interiors once the global graph avoids all of them.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.injective_closeCellwiseMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hside : A.GraphAvoidsInteriors)
:
Graph-side compatibility makes the coherent close cellwise filling injective.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.closeCellwiseMap_isEmbedding
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hvertices : A.VerticesAvoidClosedRegions)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.range_closeCellwiseMap
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.exists_targetComplex
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
:
∃ (L : PlaneComplex), L.support = Set.range A.closeCellwiseMap ∧ L.IsPure2
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.exists_retriangulation
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
{ε : ℝ}
(A : CloseGraphApproximation ε)
(hvertices : A.VerticesAvoidClosedRegions)
:
∃ (L : PlaneComplex) (_ : L.IsPure2) (e : ↑L.support ≃ₜ K.realization),
∀ (p : ↑L.support), A.closeCellwiseMap (e p) = ↑p
A compatible close cellwise filling presents the intrinsic source as one finite pure plane complex.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_intrinsic_pl_approximation
(K : IntrinsicTwoComplex)
{h : K.realization → Plane}
(hcont : Continuous h)
(hinj : Function.Injective h)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (L : PlaneComplex) (_ : L.IsPure2) (e : ↑L.support ≃ₜ K.realization), ∀ (p : ↑L.support), dist (↑p) (h (e p)) < ε
Intrinsic-source form of Moise Ch. 6, Thm. 3. A continuous embedding of a finite intrinsic two-complex into the plane can be replaced by a finite pure plane triangulation whose coordinate embedding is uniformly close to the original one.