The interior homeomorphism

This module starts the quantitative recursion at the canonical initial matched pair. It closes the construction of the nested stage sequence and therefore obtains the limit homeomorphism between the inside of an arbitrary Jordan curve and the open square.

theorem Schoenflies.IsHomeoOn.toIsSetHomeoOn {u v : Plane → Plane} {X Y : Set Plane} (h : IsHomeoOn u v X Y) : IsSetHomeoOn u v X Y

The initial-pair interface and the endgame interface express the same restricted homeomorphism data with fields in a different order.

noncomputable def Schoenflies.prescribedAnchoredInitialData {C : Set Plane} (hC : IsJordanCurve C) (u v : Plane → Plane) (hu : IsHomeoOn u v C modelCurve) : AnchoredInitialData C (anchorSet hC)

The anchored initial pair using the boundary homeomorphism supplied by the caller.

Equations

• Schoenflies.prescribedAnchoredInitialData hC u v hu = ⋯.choose

theorem Schoenflies.prescribedAnchoredInitialData_u {C : Set Plane} (hC : IsJordanCurve C) (u v : Plane → Plane) (hu : IsHomeoOn u v C modelCurve) : (prescribedAnchoredInitialData hC u v hu).u = u

noncomputable def Schoenflies.prescribedJordanStageSequence {C : Set Plane} (hC : IsJordanCurve C) (u v : Plane → Plane) (hu : IsHomeoOn u v C modelCurve) : StageSequence InitialCell initialStructure C

The quantitative sequence starting with a prescribed boundary homeomorphism.

Equations

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

noncomputable def Schoenflies.jordanStageSequence {C : Set Plane} (hC : IsJordanCurve C) : StageSequence InitialCell initialStructure C

The canonical, fully quantitative sequence of matched subdivisions associated with a Jordan curve.

Equations

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

theorem Schoenflies.exists_isHomeoOn_inside_openSquare {C : Set Plane} (hC : IsJordanCurve C) : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G (inside C) (Plane.openSquare 0 1)

prop:interior-homeomorphism. Every Jordan curve bounds a domain homeomorphic to the open square.

noncomputable def Schoenflies.jordanInteriorMap {C : Set Plane} (hC : IsJordanCurve C) : Plane → Plane

The selected limit map on the open Jordan domain.

Equations

• Schoenflies.jordanInteriorMap hC = (Schoenflies.jordanStageSequence hC).limitTower.F

noncomputable def Schoenflies.jordanInteriorInv {C : Set Plane} (hC : IsJordanCurve C) : Plane → Plane

The selected inverse limit map on the open square.

Equations

• Schoenflies.jordanInteriorInv hC = (Schoenflies.jordanStageSequence hC).limitTower.inv

theorem Schoenflies.jordanInteriorMap_isHomeoOn {C : Set Plane} (hC : IsJordanCurve C) : IsHomeoOn (jordanInteriorMap hC) (jordanInteriorInv hC) (inside C) (Plane.openSquare 0 1)

theorem Schoenflies.jordanInteriorMap_eq_initialData_u {C : Set Plane} (hC : IsJordanCurve C) : Set.EqOn (jordanInteriorMap hC) (initialData hC).u C

The limit map already agrees with the prescribed initial boundary homeomorphism wherever the latter is evaluated on the Jordan curve. Schoenflies/BoundaryAnchors.lean supplies the additional data used to prove boundary continuity.

theorem Schoenflies.prescribedJordanStageSequence_F_eq_boundary {C : Set Plane} (hC : IsJordanCurve C) (u v : Plane → Plane) (hu : IsHomeoOn u v C modelCurve) : Set.EqOn (prescribedJordanStageSequence hC u v hu).limitTower.F u C

The limit map selected from the prescribed initial pair agrees pointwise with the caller's boundary homeomorphism.