Documentation

TauCeti.Analysis.Complex.PlaneSeparation.LocalSeparation

Complementary components at a straight point of a Jordan curve #

If a Jordan curve agrees locally with a line at one point, it has at most one bounded complementary component. In particular, any bounded complementary component is the entire filled hull minus the curve. This identifies the inside of a simple polygon from any one of its bounded complementary components, without a convexity assumption.

An interior point of a nondegenerate straight segment has a ball in which the segment agrees with its supporting line. This supplies the local line hypothesis for polygonal curves.

The more general local-cover result bounds the number of complementary components by two whenever a neighbourhood of a curve point, minus the curve, is covered by two preconnected subsets of the complement. Every complementary component approaches that point, so three different components would have to meet the same local side.

Such a curve also has at least one bounded complementary component: this is the separation half of the Jordan curve theorem for Jordan curves with a straight piece, polygons among them. Points on opposite sides of the straight piece lie in different components of the complement by the segment-crossing theorem TauCeti.Contour.notMem_connectedComponentIn_compl_of_isPreconnected_sdiff_singleton. Consequently exactly one of the two sides lies inside the curve, the inside is nonempty, and its frontier is the whole curve.

Main results #

References #

source
theorem TauCeti.IsJordanCurve.connectedComponentIn_eq_or_eq_of_local_cover {C W S T : Set ℂ} (hC : IsJordanCurve C) {p x y z : ℂ} (hp : p ∈ C) (hW : IsOpen W) (hpW : p ∈ W) (hcover : W \ C ⊆ S ∪ T) (hS : IsPreconnected S) (hT : IsPreconnected T) (hSC : S ⊆ Cᶜ) (hTC : T ⊆ Cᶜ) (hx : x ∉ C) (hy : y ∉ C) (hz : z ∉ C) (hxy : y ∉ connectedComponentIn Cᶜ x) :
connectedComponentIn Cᶜ z = connectedComponentIn Cᶜ x ∨ connectedComponentIn Cᶜ z = connectedComponentIn Cᶜ y

If two preconnected subsets of the complement cover the complement locally at a point of a Jordan curve, every complementary component is one of any two distinct components.

source
theorem TauCeti.IsJordanCurve.filledHull_sdiff_eq_connectedComponentIn_of_locally_eq_line {C : Set ℂ} (hC : IsJordanCurve C) {p x : ℂ} {r : ℝ} (hr : 0 < r) (v : ℂ) (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) (hx : x ∈ filledHull C \ C) :
filledHull C \ C = connectedComponentIn Cᶜ x

If a Jordan curve agrees with a line in a neighbourhood of one of its points, its filled hull minus the curve is any bounded complementary component. The point x selects such a component; no convexity of the curve or of that component is required.

source
theorem TauCeti.exists_ball_openSegment_eq_line {a b w : ℂ} (hab : a ≠ b) (hw : w ∈ openSegment ℝ a b) :
∃ r > 0, ∀ z ∈ Metric.ball w r, z ∈ openSegment ℝ a b ↔ ((b - a)⁻¹ * (z - w)).im = 0

Near an interior point of a nondegenerate complex line segment, the segment agrees with its supporting real line. The line is expressed in the coordinate obtained by dividing by b - a.

A straight piece of a Jordan curve separates its two sides #

source
theorem TauCeti.mem_connectedComponentIn_of_locally_subset_line_of_im_pos {C : Set ℂ} {p v x y : ℂ} {r : ℝ} (hline : ∀ z ∈ Metric.ball p r, z ∈ C → (v * (z - p)).im = 0) (hx : x ∈ Metric.ball p r) (hy : y ∈ Metric.ball p r) (hx' : 0 < (v * (x - p)).im) (hy' : 0 < (v * (y - p)).im) :
y ∈ connectedComponentIn Cᶜ x

Two points of ball p r on the same open side of a line through p lie in the same component of the complement of a curve contained in that line within ball p r: the open half-ball between them is convex and misses the curve.

source
theorem TauCeti.IsJordanCurve.notMem_connectedComponentIn_of_locally_eq_line {C : Set ℂ} (hC : IsJordanCurve C) {p v a b : ℂ} {r : ℝ} (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) (ha : a ∈ Metric.ball p r) (hb : b ∈ Metric.ball p r) (ha' : 0 < (v * (a - p)).im) (hb' : (v * (b - p)).im < 0) :
b ∉ connectedComponentIn Cᶜ a

A Jordan curve separates the two sides of a straight piece. If a Jordan curve C agrees in ball p r with the line {z | (v * (z - p)).im = 0}, then two points of that ball on opposite sides of the line lie in different components of the complement of C.

source
theorem TauCeti.IsJordanCurve.mem_filledHull_iff_notMem_filledHull_of_locally_eq_line {C : Set ℂ} (hC : IsJordanCurve C) {p v a b : ℂ} {r : ℝ} (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) (ha : a ∈ Metric.ball p r) (hb : b ∈ Metric.ball p r) (ha' : 0 < (v * (a - p)).im) (hb' : (v * (b - p)).im < 0) :
a ∈ filledHull C ↔ b ∉ filledHull C

Exactly one side of a straight piece of a Jordan curve lies inside it. If a Jordan curve C agrees in ball p r with the line {z | (v * (z - p)).im = 0}, and a, b are points of that ball on opposite sides of the line, then exactly one of them lies in the filled hull of C, that is, in a bounded component of the complement of C.

source
theorem TauCeti.IsJordanCurve.nonempty_filledHull_sdiff_of_locally_eq_line {C : Set ℂ} (hC : IsJordanCurve C) {p v : ℂ} {r : ℝ} (hr : 0 < r) (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) :
(filledHull C \ C).Nonempty

A Jordan curve with a straight piece has an inside. If a Jordan curve C agrees with a line in a ball about one of its points, then its filled hull minus C — the union of the bounded components of the complement of C — is nonempty.

source
theorem TauCeti.IsJordanCurve.frontier_filledHull_sdiff_of_locally_eq_line {C : Set ℂ} (hC : IsJordanCurve C) {p v : ℂ} {r : ℝ} (hr : 0 < r) (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) :
frontier (filledHull C \ C) = C

A Jordan curve with a straight piece bounds its inside. If a Jordan curve C agrees with a line in a ball about one of its points, then the frontier of its filled hull minus C is C.