A segment crossing a set once has its ends on different sides

A closed set K ⊆ ℂ with K \ {p} preconnected, crossed once by a straight segment at p with K adherent from both sides, separates the two ends into different connected components of Kᶜ. The proof uses winding numbers and needs no Jordan curve theorem.

This is the planar-separation input for layer L5 of the ConformalMapping roadmap.

Main results

• TauCeti.Contour.notMem_connectedComponentIn_compl_of_isPreconnected_sdiff_singleton — the two ends of the segment lie in different components of Kᶜ.
• TauCeti.Contour.mem_filledHull_or_mem_filledHull_of_isPreconnected_sdiff_singleton — for bounded K, one end lies in the filled hull.

References

• L. Ahlfors, Complex Analysis, Chapter 4, §2.1.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Section 2.2.

theorem TauCeti.Contour.notMem_connectedComponentIn_compl_of_isPreconnected_sdiff_singleton {K : Set ℂ} {v z₀ : ℂ} {a b s : ℝ} (hK : IsClosed K) (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) (hseg : ∀ t ∈ Set.Icc a b, v * ↑t + z₀ ∈ K → t = s) (hKp : IsPreconnected (K \ {v * ↑s + z₀})) (hleft : v * ↑s + z₀ ∈ closure (K ∩ {q : ℂ | 0 < ((q - (v * ↑s + z₀)) / v).im})) (hright : v * ↑s + z₀ ∈ closure (K ∩ {q : ℂ | ((q - (v * ↑s + z₀)) / v).im < 0})) : v * ↑b + z₀ ∉ connectedComponentIn Kᶜ (v * ↑a + z₀)

A segment crossing a set once has its ends in different components of the complement. Let K be closed with K \ {p} preconnected, crossed by a straight segment at an interior point p = v · s + z₀ with K adherent from both sides of the segment. Then the two endpoints v · a + z₀ and v · b + z₀ lie in different connected components of Kᶜ.

theorem TauCeti.Contour.mem_filledHull_or_mem_filledHull_of_isPreconnected_sdiff_singleton {K : Set ℂ} {v z₀ : ℂ} {a b s : ℝ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (hv : v ≠ 0) (hs : s ∈ Set.Ioo a b) (hseg : ∀ t ∈ Set.Icc a b, v * ↑t + z₀ ∈ K → t = s) (hKp : IsPreconnected (K \ {v * ↑s + z₀})) (hleft : v * ↑s + z₀ ∈ closure (K ∩ {q : ℂ | 0 < ((q - (v * ↑s + z₀)) / v).im})) (hright : v * ↑s + z₀ ∈ closure (K ∩ {q : ℂ | ((q - (v * ↑s + z₀)) / v).im < 0})) : v * ↑a + z₀ ∈ filledHull K ∨ v * ↑b + z₀ ∈ filledHull K

One end of a segment crossing a bounded set once lies in its filled hull. Under the same hypotheses as notMem_connectedComponentIn_compl_of_isPreconnected_sdiff_singleton, plus boundedness of K, at least one of v · a + z₀ and v · b + z₀ lies in filledHull K.