Set algebra for assembled polygonal-arc side strips

Proved

PolygonalArcSideStripSetAlgebra

by xuanji · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-consequencesgeometrypolygonal-arcs

Given the middle tubes, vertex collars, and local side pieces, define the global collar and its left and right strips by union. Then each strip is disjoint from the arc, the two strips are disjoint from each other, and deleting the relative interior of the arc from the collar gives exactly the union of the two strips.

Preamble

import Definitions.Def_PolygonalArcCollarLocalSideData

open Classical
noncomputable section

Formal statement

lemma PolygonalArcSideStripSetAlgebra
    (γ : PolygonalArc) {η : ℝ}
    (controlRadii : PolygonalArcCollarControlRadii γ η)
    (middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
    (forbiddenMargins :
      PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
    (orientedTubes : PolygonalArcCollarOrientedSeparatedTubeData γ controlRadii middleSegments
        forbiddenMargins)
    (vertexLocalPieces :
      PolygonalArcCollarVertexLocalPieceData γ controlRadii middleSegments
        forbiddenMargins orientedTubes.toPolygonalArcCollarSeparatedTubeData)
    (localSideData :
      PolygonalArcCollarLocalSideData γ controlRadii middleSegments
        forbiddenMargins orientedTubes vertexLocalPieces) :
    let sep := orientedTubes.toPolygonalArcCollarSeparatedTubeData
    let C : Set (EuclideanSpace ℝ (Fin 2)) :=
      ((⋃ (j : ℕ), ⋃ (hj : j + 1 < γ.vertices.length), sep.tube j hj) ∪
        (⋃ i : Fin γ.vertices.length, localSideData.vertexCollar i))
    let L : Set (EuclideanSpace ℝ (Fin 2)) :=
      ((⋃ (j : ℕ), ⋃ (hj : j + 1 < γ.vertices.length), sep.leftHalf j hj) ∪
        (⋃ i : Fin γ.vertices.length, localSideData.leftSidePiece i))
    let R : Set (EuclideanSpace ℝ (Fin 2)) :=
      ((⋃ (j : ℕ), ⋃ (hj : j + 1 < γ.vertices.length), sep.rightHalf j hj) ∪
        (⋃ i : Fin γ.vertices.length, localSideData.rightSidePiece i))
    Disjoint L γ.carrier ∧ Disjoint R γ.carrier ∧ Disjoint L R ∧
      C \ γ.relativeInterior = L ∪ R := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcSideStripSetAlgebra.lean#L1-L33

View graph