Matching and cutting simple polygonal arcs

An ear can have an arbitrary finite number of abstract edges. On the target side we only obtain one set-level polygonal crosscut. This module supplies the two facts that reconcile those descriptions.

• Two named arcs admit an endpoint-preserving homeomorphism, obtained by matching their parameters.
• An arc contained in a polygonal arc is polygonal. Consequently the images of all source edge arcs under the parameter-matching homeomorphism are polygonal target edge arcs.

The inverse of a compact parametrisation

theorem Schoenflies.continuousOn_invFunOn_image' {f : ℝ → Plane} {s : Set ℝ} (hs : IsCompact s) (hf : ContinuousOn f s) (hinj : Set.InjOn f s) : ContinuousOn (Function.invFunOn f s) (f '' s)

A continuous injection of a compact set has a continuous invFunOn on its image.

A subarc of a polygonal arc is polygonal

theorem Schoenflies.IsArcBetween.eq_of_subset_arc {A B C : Set Plane} {p q r s : Plane} (hA : IsArcBetween A p q) (hB : IsArcBetween B p q) (hC : IsArcBetween C r s) (hAC : A ⊆ C) (hBC : B ⊆ C) : A = B

An arc contained in another arc is the unique closed subarc between its two endpoints. This form allows the ambient arc to have different endpoints.

theorem Schoenflies.IsArcBetween.isPolygonal_of_subset_arc {A C : Set Plane} {p q r s : Plane} (hA : IsArcBetween A p q) (hC : IsArcBetween C r s) (hpoly : IsPolygonal C) (hAC : A ⊆ C) : IsPolygonal A

Every closed subarc of a polygonal arc is polygonal.

Matching two named arcs

structure Schoenflies.ArcHomeo (A B : Set Plane) (a b c d : Plane) : Type

A homeomorphism between two arcs, with the named endpoints matched in order. The maps are total functions because that is the shape needed by the split constructor; all inverse and continuity assertions are restricted to the two arc carriers.

• toFun : Plane → Plane

  Forward map, with continuity and inverse laws restricted to the arcs.

• invFun : Plane → Plane

  Inverse map on the target arc.

• continuousOn_toFun : ContinuousOn self.toFun A
• continuousOn_invFun : ContinuousOn self.invFun B
• leftInvOn : Set.LeftInvOn self.invFun self.toFun A
• rightInvOn : Set.RightInvOn self.invFun self.toFun B
• image_eq : self.toFun '' A = B
• map_left : self.toFun a = c
• map_right : self.toFun b = d

theorem Schoenflies.ArcHomeo.injOn {A B : Set Plane} {a b c d : Plane} (h : ArcHomeo A B a b c d) : Set.InjOn h.toFun A

theorem Schoenflies.ArcHomeo.mapsTo {A B : Set Plane} {a b c d : Plane} (h : ArcHomeo A B a b c d) : Set.MapsTo h.toFun A B

theorem Schoenflies.ArcHomeo.mapsTo_invFun {A B : Set Plane} {a b c d : Plane} (h : ArcHomeo A B a b c d) : Set.MapsTo h.invFun B A

theorem Schoenflies.exists_arcHomeo {A B : Set Plane} {a b c d : Plane} (hA : IsArcBetween A a b) (hB : IsArcBetween B c d) : Nonempty (ArcHomeo A B a b c d)

Any two named arcs admit an endpoint-preserving homeomorphism.

Transporting a plane drawing along an arc homeomorphism

def Graph.mapDrawing {β : Type u_1} {A B : Set Schoenflies.Plane} {a b c d : Schoenflies.Plane} (m : Schoenflies.ArcHomeo A B a b c d) (drawing : β → ℝ → Schoenflies.Plane) : β → ℝ → Schoenflies.Plane

Apply the map of an arc homeomorphism to every edge parametrisation.

Equations

• Graph.mapDrawing m drawing e t = m.toFun (drawing e t)

theorem Graph.edgeArc_mapDrawing {β : Type u_1} {A B : Set Schoenflies.Plane} {a b c d : Schoenflies.Plane} {drawing : β → ℝ → Schoenflies.Plane} (m : Schoenflies.ArcHomeo A B a b c d) (e : β) : edgeArc (mapDrawing m drawing) e = m.toFun '' edgeArc drawing e

theorem Graph.pointSet_map_mapDrawing {β : Type u_1} {A B : Set Schoenflies.Plane} {a b c d : Schoenflies.Plane} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (m : Schoenflies.ArcHomeo A B a b c d) : (map m.toFun G).pointSet (mapDrawing m drawing) = m.toFun '' G.pointSet drawing

theorem Graph.IsDrawing.map_arcHomeo {β : Type u_1} {A B : Set Schoenflies.Plane} {a b c d : Schoenflies.Plane} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) (m : Schoenflies.ArcHomeo A B a b c d) (hpoint : G.pointSet drawing = A) : (map m.toFun G).IsDrawing (mapDrawing m drawing)

A drawing whose whole point set is one arc transports along an arc homeomorphism.