Cutting a segment

Mathlib has no lemma splitting a segment at an interior point, and the polygonal subdivision of Layer 6 is built entirely out of one: cutting loses nothing (segment_split) and cutting is permanent (openSegment_left_subset, openSegment_right_subset — each half's interior stays inside the whole's, so nothing later can put a removed point back into an interior).

Everything here is an identity between convex combinations. The ⊇ half of the split is convexity; the ⊆ half rescales the parameter, and the only case analysis is on whether the far coefficient vanishes.

Blueprint

• segment_split — cutting at a point of the segment loses nothing; underneath subdivide_covers.
• openSegment_left_subset, openSegment_right_subset — a cut is permanent; underneath subdivide_inside.

theorem Schoenflies.segment_split {a b p : Plane} (hp : p ∈ segment ℝ a b) : segment ℝ a b = segment ℝ a p ∪ segment ℝ p b

Cutting a segment at one of its points loses nothing: the two halves cover it.

theorem Schoenflies.openSegment_left_subset {a b p : Plane} (hp : p ∈ openSegment ℝ a b) : openSegment ℝ a p ⊆ openSegment ℝ a b

Cutting is permanent, near half: the interior of the near piece stays inside the interior of the whole.

theorem Schoenflies.openSegment_right_subset {a b p : Plane} (hp : p ∈ openSegment ℝ a b) : openSegment ℝ p b ⊆ openSegment ℝ a b

Cutting is permanent, far half.