Prove2Me

Basic topology of polygonal-arc middle tubes

Proved
PolygonalArcMiddleTubeBasicTopology

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

crossing-consequencesgeometrypolygonal-arcs

For every middle segment of a polygonal arc, the associated separated tube and its two oriented half-tubes are open, and each half-tube is connected. This is the local topological input used when assembling the global left and right side strips.

Preamble
import Definitions.Def_PolygonalArcCollarOrientedSeparatedTubeData
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
import Mathlib.Topology.Algebra.Module.FiniteDimension

open Classical
noncomputable section
Formal statement
lemma PolygonalArcMiddleTubeBasicTopology
    (γ : PolygonalArc) {η : ℝ}
    (controlRadii : PolygonalArcCollarControlRadii γ η)
    (middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
    (forbiddenMargins :
      PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
    (orientedTubes :
      PolygonalArcCollarOrientedSeparatedTubeData γ controlRadii middleSegments
        forbiddenMargins) :
    (∀ (j : ℕ) (hj : j + 1 < γ.vertices.length),
      IsOpen (orientedTubes.toPolygonalArcCollarSeparatedTubeData.tube j hj)) ∧
    (∀ (j : ℕ) (hj : j + 1 < γ.vertices.length),
      IsOpen (orientedTubes.toPolygonalArcCollarSeparatedTubeData.leftHalf j hj)) ∧
    (∀ (j : ℕ) (hj : j + 1 < γ.vertices.length),
      IsOpen (orientedTubes.toPolygonalArcCollarSeparatedTubeData.rightHalf j hj)) ∧
    (∀ (j : ℕ) (hj : j + 1 < γ.vertices.length),
      IsConnected (orientedTubes.toPolygonalArcCollarSeparatedTubeData.leftHalf j hj)) ∧
    (∀ (j : ℕ) (hj : j + 1 < γ.vertices.length),
      IsConnected (orientedTubes.toPolygonalArcCollarSeparatedTubeData.rightHalf j hj)) := by sorry
Source
https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcMiddleTubeBasicTopology.lean#L1-L27

View graph