Along one segment: the distance from an end as a coordinate

Everything the polygonal overlay has to say about several collinear segments — which piece lies inside which, where a piece may end, when two pieces have to coincide — is one-dimensional: it happens along a single straight segment. This module supplies the coordinate that makes it ordinary arithmetic. Along a nondegenerate segment ℝ a b the distance from a determines the point, and it reads betweenness off as a pair of inequalities, so a claim about four collinear points becomes a claim about four reals.

No new geometry is needed. dist_left_lineMap already says the distance from a is the parameter of AffineMap.lineMap a b, scaled by the segment's length, and image_segment already says that parametrization carries segments of ℝ to segments of the plane. What is added here is the translation, stated once so that the arithmetic does not have to be redone at every use.

The two results the module exists for come last, and they are what makes cutting at every meet enough:

• a piece that meets an overlap and keeps the overlap's ends out of its interior lies inside the overlap (segment_inside_of_ends_outside);
• two pieces whose interiors meet, each keeping the other's ends out of its interior, are the same pair of points (same_ends_of_meeting_interiors).

Both are stated inside one ambient segment. Collinearity is not optional: a piece crossing the overlap transversally would meet it and avoid both its ends without lying inside it, so every point named is a point of one ambient segment ℝ a b.

Both are also stated with no orientation asked of the caller. The _oriented forms they wrap are near-end-first, which is what the arithmetic wants; the unoriented forms decide the orientation themselves, and they are what the overlay uses.

A note on degenerate pieces

Mathlib's openSegment ℝ u u is {u}, not ∅. A degenerate piece therefore has a nonempty interior, and the strict translation dist_lt_of_mem_openSegment genuinely needs u ≠ v. The two headline theorems do not ask for it: in each of them a degenerate piece is either excluded by the hypotheses or settled outright, and that case split lives inside the proof.

Blueprint

• segment_inside_of_ends_outside, same_ends_of_meeting_interiors — the separation behind the deduplication clause of the polygonal overlay (lem:polygonal-overlay, "represent every duplicate geometric subsegment only once") and of the subdivision in lem:polygonal-connected ("delete duplicate subsegments"): once every piece's ends are cut points, and so interior to nothing, two pieces that share an interior point coincide instead of merely overlapping.

The parametrization of a segment

AffineMap.lineMap a b walks from a to b. It carries a segment of ℝ onto the corresponding piece of [a, b], and it turns the distance from a into multiplication by the segment's length. Those two facts are the whole content of the module; the rest is arithmetic.

theorem Schoenflies.dist_left_lineMap_of_nonneg (a b : Plane) {t : ℝ} (ht : 0 ≤ t) : dist a ((AffineMap.lineMap a b) t) = t * dist a b

The distance from the left endpoint to the point at parameter t is t times the segment's length. This is dist_left_lineMap with the absolute value discharged.

theorem Schoenflies.segment_lineMap_image (a b : Plane) (p q : ℝ) : segment ℝ ((AffineMap.lineMap a b) p) ((AffineMap.lineMap a b) q) = ⇑(AffineMap.lineMap a b) '' segment ℝ p q

The piece of [a, b] spanned by two parameters is the image of the segment they span.

theorem Schoenflies.openSegment_lineMap_image (a b : Plane) (p q : ℝ) : openSegment ℝ ((AffineMap.lineMap a b) p) ((AffineMap.lineMap a b) q) = ⇑(AffineMap.lineMap a b) '' openSegment ℝ p q

The same for interiors.

theorem Schoenflies.exists_param_of_mem_segment {a b x : Plane} (hx : x ∈ segment ℝ a b) : ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ (AffineMap.lineMap a b) t = x ∧ dist a x = t * dist a b

Every point of [a, b] carries a parameter: a number t ∈ [0, 1] placing it on the segment, whose distance from a is t times the segment's length. This is the only way the rest of the module looks at a point of the segment.

The coordinate

theorem Schoenflies.parameter_le_of_distance {a b : Plane} (hab : a ≠ b) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : dist a ((AffineMap.lineMap a b) s) ≤ dist a ((AffineMap.lineMap a b) t)) : s ≤ t

Along a nondegenerate segment, the distance from the left endpoint orders the parameters: a nonzero length cancels from s * ‖b - a‖ ≤ t * ‖b - a‖.

theorem Schoenflies.eq_of_dist_left_eq {a b : Plane} (hab : a ≠ b) {x y : Plane} (hx : x ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) (h : dist a x = dist a y) : x = y

The distance from a determines the point: two points of a nondegenerate [a, b] at equal distance from a are equal.

Betweenness as a pair of inequalities

theorem Schoenflies.dist_le_of_mem_segment {a b : Plane} (hab : a ≠ b) {u v x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (huv : dist a u ≤ dist a v) (hx : x ∈ segment ℝ u v) : dist a u ≤ dist a x ∧ dist a x ≤ dist a v

A point between two points of the segment is between them in distance from a as well: measured from a, the nearer end comes first.

theorem Schoenflies.mem_segment_of_dist_le {a b : Plane} (hab : a ≠ b) {u v x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hx : x ∈ segment ℝ a b) (h₁ : dist a u ≤ dist a x) (h₂ : dist a x ≤ dist a v) : x ∈ segment ℝ u v

The converse: a point of the segment whose distance from a lies between the two ends' distances lies between the ends.

The same translation for interiors

openSegment ℝ u u = {u} in Mathlib, so the strict form asks for a nondegenerate piece; its converse does not, since strict inequalities force nondegeneracy on their own.

theorem Schoenflies.dist_lt_of_mem_openSegment {a b : Plane} (hab : a ≠ b) {u v x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (huv : u ≠ v) (hor : dist a u ≤ dist a v) (hx : x ∈ openSegment ℝ u v) : dist a u < dist a x ∧ dist a x < dist a v

A point interior to a nondegenerate piece of the segment is strictly between its ends in distance from a.

theorem Schoenflies.mem_openSegment_of_dist_lt {a b : Plane} (hab : a ≠ b) {u v x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hx : x ∈ segment ℝ a b) (h₁ : dist a u < dist a x) (h₂ : dist a x < dist a v) : x ∈ openSegment ℝ u v

The converse: a point of the segment strictly between the ends in distance from a is interior to the piece they span.

Where a point that is not interior to a piece must sit

These two carry the whole one-dimensional argument. A point of the ambient segment kept out of a piece's interior has to be outside on one side or the other, and knowing which side it is not settles it.

theorem Schoenflies.dist_le_left_of_notMem_openSegment {a b : Plane} (hab : a ≠ b) {u v y : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) (hout : y ∉ openSegment ℝ u v) (hlt : dist a y < dist a v) : dist a y ≤ dist a u

A point of the ambient segment kept out of [u, v]'s interior and lying before v lies at or before u.

theorem Schoenflies.le_dist_right_of_notMem_openSegment {a b : Plane} (hab : a ≠ b) {u v y : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) (hout : y ∉ openSegment ℝ u v) (hlt : dist a u < dist a y) : dist a v ≤ dist a y

The mirror: a point of the ambient segment kept out of [u, v]'s interior and lying after u lies at or after v.

What the overlay is after

theorem Schoenflies.segment_inside_of_ends_outside_oriented {a b : Plane} (hab : a ≠ b) {u v s t x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hpiece : dist a u ≤ dist a v) (hs : s ∈ segment ℝ a b) (ht : t ∈ segment ℝ a b) (hover : dist a s ≤ dist a t) (hxp : x ∈ openSegment ℝ u v) (hxo : x ∈ openSegment ℝ s t) (hsout : s ∉ openSegment ℝ u v) (htout : t ∉ openSegment ℝ u v) : segment ℝ u v ⊆ segment ℝ s t

A piece that meets an overlap and keeps the overlap's two ends out of its interior lies inside the overlap — near-end-first form.

theorem Schoenflies.same_ends_of_meeting_interiors_oriented {a b : Plane} (hab : a ≠ b) {u v s t x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hfirst : dist a u ≤ dist a v) (hs : s ∈ segment ℝ a b) (ht : t ∈ segment ℝ a b) (hsecond : dist a s ≤ dist a t) (hxu : x ∈ openSegment ℝ u v) (hxs : x ∈ openSegment ℝ s t) (hsout : s ∉ openSegment ℝ u v) (htout : t ∉ openSegment ℝ u v) (huout : u ∉ openSegment ℝ s t) (hvout : v ∉ openSegment ℝ s t) : u = s ∧ v = t

Two pieces of one ambient segment whose interiors meet, each keeping the other's ends out of its interior, have the same ends — near-end-first form.

The same two, asking the caller nothing about orientation

A piece is a pair of ends, and which of them is nearer a is none of the caller's business — segment and openSegment do not care. The oriented forms above are near-end-first because that is what the arithmetic wants; these decide the orientation themselves. Every hypothesis is restated in both spellings first, so each of the four cases is just "which way round, then cite".

theorem Schoenflies.segment_inside_of_ends_outside {a b : Plane} (hab : a ≠ b) {u v s t x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hs : s ∈ segment ℝ a b) (ht : t ∈ segment ℝ a b) (hxp : x ∈ openSegment ℝ u v) (hxo : x ∈ openSegment ℝ s t) (hsout : s ∉ openSegment ℝ u v) (htout : t ∉ openSegment ℝ u v) : segment ℝ u v ⊆ segment ℝ s t

A piece that meets an overlap and keeps the overlap's two ends out of its interior lies inside the overlap.

Collinearity is not optional: every point named is a point of one ambient segment ℝ a b. A piece crossing the overlap transversally would meet it and avoid both its ends without lying inside it.

theorem Schoenflies.same_ends_of_meeting_interiors {a b : Plane} (hab : a ≠ b) {u v s t x : Plane} (hu : u ∈ segment ℝ a b) (hv : v ∈ segment ℝ a b) (hs : s ∈ segment ℝ a b) (ht : t ∈ segment ℝ a b) (hxu : x ∈ openSegment ℝ u v) (hxs : x ∈ openSegment ℝ s t) (hsout : s ∉ openSegment ℝ u v) (htout : t ∉ openSegment ℝ u v) (huout : u ∉ openSegment ℝ s t) (hvout : v ∉ openSegment ℝ s t) : u = s ∧ v = t ∨ u = t ∧ v = s

Two pieces of one ambient segment whose interiors meet, each keeping the other's ends out of its interior, are the same pair of points — in one order or the other.

This is the separation the deduplication clause is for: overlapping collinear pieces cannot be pulled apart by cutting, and after enough cuts they coincide instead.