Broken-line connectivity of open connected sets in the plane

Moise, Geometric Topology in Dimensions 2 and 3, Ch. 1: any two points of an open connected subset of the plane are joined by a broken line (a finite polygonal chain of straight segments) lying in the set. This is the elementary input to the PL-approximation chapter (Thm 6.1); see the docstrings of ClassificationOfSurfaces/Moise/PLApproximation.lean for the wider context.

JoinedByBrokenLine U a b records a chain of n segments inside U from a to b, as a vertex list v : Fin (n + 1) → Plane whose consecutive closed segments all lie in U. The relation is reflexive (at points of U), symmetric, transitive, and monotone in U.

The main theorem IsPreconnected.joinedByBrokenLine is the standard clopen-chain argument: for fixed a, both {x ∈ U | JoinedByBrokenLine U a x} and its complement in U are open, because any metric ball inside U is convex, so the segment from a ball's centre to any of its points extends or truncates a broken line by one segment. Preconnectedness of U then forces the complement to be empty.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine (U : Set Plane) (a b : Plane) : Prop

a and b are joined by a broken line inside U: there is a finite chain of vertices starting at a and ending at b such that every consecutive closed segment lies in U.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.of_segment {U : Set Plane} {a b : Plane} (h : segment ℝ a b ⊆ U) : JoinedByBrokenLine U a b

A single segment inside U is a broken line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.refl {U : Set Plane} {a : Plane} (ha : a ∈ U) : JoinedByBrokenLine U a a

Any point of U is joined to itself by a (degenerate) broken line in U.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.symm {U : Set Plane} {a b : Plane} (h : JoinedByBrokenLine U a b) : JoinedByBrokenLine U b a

Broken-line connectivity is symmetric: traverse the chain backwards.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.snoc {U : Set Plane} {a b c : Plane} (hab : JoinedByBrokenLine U a b) (hseg : segment ℝ b c ⊆ U) : JoinedByBrokenLine U a c

Extend a broken line from a to b by one further segment from b to c inside U.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.trans {U : Set Plane} {a b c : Plane} (hab : JoinedByBrokenLine U a b) (hbc : JoinedByBrokenLine U b c) : JoinedByBrokenLine U a c

Broken-line connectivity is transitive: concatenate the two chains.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.JoinedByBrokenLine.mono {U V : Set Plane} {a b : Plane} (h : JoinedByBrokenLine U a b) (hUV : U ⊆ V) : JoinedByBrokenLine V a b

Transport a broken line along an inclusion U ⊆ V.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPreconnected.joinedByBrokenLine {U : Set Plane} (hU : IsOpen U) (hconn : IsPreconnected U) {a b : Plane} (ha : a ∈ U) (hb : b ∈ U) : JoinedByBrokenLine U a b

Broken-line connectivity (Moise, Ch. 1): any two points of an open preconnected subset of the plane are joined by a broken line lying in the set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsPreconnected.thickening {A : Set Plane} (hA : IsPreconnected A) {ε : ℝ} : 0 < ε → IsPreconnected (Metric.thickening ε A)

A positive metric thickening of a preconnected plane set is preconnected.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.brokenLine_in_thickening_of_preconnected {A : Set Plane} (hA : IsPreconnected A) {a b : Plane} (ha : a ∈ A) (hb : b ∈ A) {ε : ℝ} (hε : 0 < ε) : JoinedByBrokenLine (Metric.thickening ε A) a b

Moise Chapter 6, Theorem 1: the endpoints of an embedded edge can be joined by a broken line in every positive metric neighborhood of its image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.brokenLine_in_thickening_inter_convexHull_of_preconnected {A : Set Plane} (hA : IsPreconnected A) {a b : Plane} (ha : a ∈ A) (hb : b ∈ A) {ε : ℝ} (hε : 0 < ε) : JoinedByBrokenLine (Metric.thickening ε A ∩ (convexHull ℝ) A) a b

A preconnected set admits broken-line approximations whose vertices stay in its convex hull.

The thickening supplies room for the polygonal chain, while convex-hull containment records the extra fact needed to preserve convex target regions such as a half-plane.