The polygonal overlay

Finitely many segments become a plane graph once they are subdivided at their meets and each duplicated subsegment is named once (lem:polygonal-overlay).

Blueprint

• polygonal_overlay — Lemma 3.7 (polygonal overlay).

Two more properties of subdivide

Both belong in Schoenflies/Subdivide.lean beside the other four; they are here because that module is on main.

subdivide_subset is subdivide_interior_subset with the closed inclusion carried alongside the open one, in one existential: separation reads a piece's ends off its source segment and its interior off the source's interior, and it needs both at the same source.

subdivide_ends is the endpoint criterion — an end of a piece that is not a cut point was an end all along. Without it the case of two pieces from different sources does not close: two different subpieces can both sit inside one long overlap.

theorem Schoenflies.splitAt_subset (p : Plane) (P Q : Piece) : Q ∈ splitAt p P → Q.seg ⊆ P.seg ∧ Q.interior ⊆ P.interior

Cutting one piece keeps each half inside the whole, closed and open at once.

theorem Schoenflies.splitAllAt_subset (p : Plane) (pieces : List Piece) (Q : Piece) : Q ∈ splitAllAt p pieces → ∃ P ∈ pieces, Q.seg ⊆ P.seg ∧ Q.interior ⊆ P.interior

theorem Schoenflies.subdivide_subset (pieces : List Piece) (points : List Plane) (Q : Piece) : Q ∈ subdivide pieces points → ∃ P ∈ pieces, Q.seg ⊆ P.seg ∧ Q.interior ⊆ P.interior

Every piece of a subdivision lies inside a piece it came from, both as a segment and as an interior — and at the same source.

theorem Schoenflies.splitAt_ends (p : Plane) (P Q : Piece) : Q ∈ splitAt p P → ∀ (z : Plane), z = Q.1 ∨ z = Q.2 → z = p ∨ z = P.1 ∨ z = P.2

Cutting one piece introduces only the cut point as a new end.

theorem Schoenflies.splitAllAt_ends (p : Plane) (pieces : List Piece) (Q : Piece) : Q ∈ splitAllAt p pieces → ∀ (z : Plane), z = Q.1 ∨ z = Q.2 → z = p ∨ ∃ P ∈ pieces, z = P.1 ∨ z = P.2

theorem Schoenflies.subdivide_ends (pieces : List Piece) (points : List Plane) (Q : Piece) : Q ∈ subdivide pieces points → ∀ (z : Plane), z = Q.1 ∨ z = Q.2 → z ∈ points ∨ ∃ P ∈ pieces, z = P.1 ∨ z = P.2

The endpoint criterion. An end of a piece of the subdivision is either a cut point or was an end of a source piece all along.

What the cut points have to cover

Two conditions, and between them they are the blueprint's "subdivide at all old endpoints, isolated intersections, and endpoints of overlapping intervals". The second asks for some pair of ends of each meet rather than every pair, because that is what a construction can supply: a meet is segment ℝ u v and segment ℝ v u alike, and that a nondegenerate segment's ends are determined by its point set is a theorem this development does not have and does not need.

def Schoenflies.meetOf (P Q : Piece) : Set Plane

Where two pieces meet.

Equations

• Schoenflies.meetOf P Q = P.seg ∩ Q.seg

theorem Schoenflies.meetOf_comm (P Q : Piece) : meetOf P Q = meetOf Q P

def Schoenflies.EndsAreCut (pieces : List Piece) (points : List Plane) : Prop

Every end of every source piece is a cut point.

Equations

• Schoenflies.EndsAreCut pieces points = ∀ P ∈ pieces, ∀ (z : Schoenflies.Plane), z = P.1 ∨ z = P.2 → z ∈ points

def Schoenflies.MeetsAreCut (pieces : List Piece) (points : List Plane) : Prop

For every pair of distinct source pieces that meet, some pair of ends of the meet is cut.

Equations

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

theorem Schoenflies.subdivide_ends_are_cuts {pieces : List Piece} {points : List Plane} (h : EndsAreCut pieces points) (Q : Piece) : Q ∈ subdivide pieces points → ∀ (z : Plane), z = Q.1 ∨ z = Q.2 → z ∈ points

With the source ends cut too, the endpoint criterion says outright that every end of every piece of the subdivision is a cut point.

Producing the cut points

Nothing computes them. The overlay is stated existentially, so the list is built by the induction that proves it exists, and segment_inter_segment hands over the ends of a meet the moment the meet is known to be nonempty. That is what keeps the choice operator out: the witnesses of segment_inter_segment are not unique, so there is nothing to name.

theorem Schoenflies.exists_meet_points (P : Piece) (others : List Piece) : ∃ (points : List Plane), ∀ Q ∈ others, (meetOf P Q).Nonempty → ∃ (u : Plane) (v : Plane), meetOf P Q = segment ℝ u v ∧ u ∈ points ∧ v ∈ points

One piece against a list: a point list holding both ends of every meet.

theorem Schoenflies.exists_cut_points (pieces : List Piece) : ∃ (points : List Plane), EndsAreCut pieces points ∧ MeetsAreCut pieces points

The whole list: the ends of each piece, and both ends of each meet. No sort and no choice operator — the point list is existential throughout.

Separation

Cut at every end of every source piece and at both ends of every meet, and two pieces of the subdivision that share an interior point are the same segment — equal, not disjoint. Overlapping collinear pieces cannot be pulled apart by cutting; after enough cuts they coincide, which is what the blueprint's deduplication clause is for.

theorem Schoenflies.subdivide_common_segment {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hMeets : MeetsAreCut pieces points) {P Q : Piece} (hP : P ∈ subdivide pieces points) (hQ : Q ∈ subdivide pieces points) {x : Plane} (hxP : x ∈ P.interior) (hxQ : x ∈ Q.interior) : ∃ (A : Piece), A.Nondeg ∧ P.seg ⊆ A.seg ∧ Q.seg ⊆ A.seg

Collinearity: two pieces of the subdivision that share an interior point lie inside one nondegenerate segment. If they came from the same source piece, that piece; if from different ones, the sources' overlap — nondegenerate because the shared point is interior to it, the overlap's ends being cut points and so interior to nothing.

theorem Schoenflies.subdivide_separated {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) {P Q : Piece} (hP : P ∈ subdivide pieces points) (hQ : Q ∈ subdivide pieces points) {x : Plane} (hxP : x ∈ P.interior) (hxQ : x ∈ Q.interior) : P = Q ∨ P = (Q.2, Q.1)

Separation. Two pieces of the subdivision that share an interior point are the same segment, in one order or the other.