Arcs do not separate the plane, and a Jordan curve bounds each of its complementary components

Borsuk's criterion TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn turns the continuous logarithm of the Borsuk map on a simple arc (TauCeti.hasContinuousLogOn_sub_div_sub_range_of_injective_path) into the classical fact that a simple arc does not separate the plane. Since a proper subcontinuum of a Jordan curve is a point or an arc, no such subcontinuum separates the plane either.

This is what shows that a Jordan curve C ⊆ ℂ is adherent to every component of its complement, as soon as the complement has two components at all: given a point q ∈ C and r > 0, cut out of C a closed arc S whose complement in the curve lies in ball q r. Two points x, y in different components of Cᶜ lie in one component D of Sᶜ, so D must meet C \ S ⊆ ball q r; walking inside D from the component E of Cᶜ containing x, one meets the frontier of E in C \ S. Hence E comes within r of q. Thus the frontier of every complementary component is the whole curve. This is the half of the Jordan curve theorem that needs no construction of an inside. Together with the empty interior of a Jordan curve (TauCeti.IsJordanCurve.interior_eq_empty) it shows that an open set contained in the filled hull of a Jordan curve does not meet the curve: such a set, if it met the curve, would contain a point off the curve in a bounded component, so the curve would separate the plane and the open set would also meet the unbounded component.

Main results

• Path.isConnected_compl_range_of_injective — the complement of a simple arc in the plane is connected.
• TauCeti.IsJordanCurve.isConnected_compl_of_ne — the complement of a proper subcontinuum of a Jordan curve in the plane is connected.
• TauCeti.IsJordanCurve.subset_closure_connectedComponentIn — if a Jordan curve separates two points, it lies in the closure of each of their complementary components.
• TauCeti.IsJordanCurve.frontier_connectedComponentIn — the frontier of such a component is the whole curve.
• TauCeti.IsJordanCurve.disjoint_of_isOpen_of_subset_filledHull — an open set contained in the filled hull of a Jordan curve misses the curve.

References

• J. R. Munkres, Topology, §61–63.
• S. Janiszewski, Sur les coupures du plan faites par les continus, Prace Mat.-Fiz. 26 (1913).

theorem Path.isConnected_compl_range_of_injective {p q : ℂ} (γ : Path p q) (hγ : Function.Injective ⇑γ) : IsConnected (Set.range ⇑γ)ᶜ

A simple arc does not separate the plane. The complement of the range of an injective path in ℂ is connected.

theorem TauCeti.IsJordanCurve.isConnected_compl_of_ne {C S : Set ℂ} (h : IsJordanCurve C) (hSC : S ⊆ C) (hS : IsCompact S) (hpre : IsPreconnected S) (hSne : S ≠ C) : IsConnected Sᶜ

A proper subcontinuum of a Jordan curve does not separate the plane. If S is a compact preconnected subset of a Jordan curve C ⊆ ℂ with S ≠ C, then Sᶜ is connected.

theorem TauCeti.IsJordanCurve.subset_closure_connectedComponentIn {C : Set ℂ} (h : IsJordanCurve C) {x y : ℂ} (hx : x ∉ C) (hy : y ∉ C) (hxy : y ∉ connectedComponentIn Cᶜ x) : C ⊆ closure (connectedComponentIn Cᶜ x)

A Jordan curve lies in the closure of each of its complementary components. If the Jordan curve C ⊆ ℂ separates x from y, then every point of C is adherent to the component of Cᶜ containing x.

theorem TauCeti.IsJordanCurve.frontier_connectedComponentIn {C : Set ℂ} (h : IsJordanCurve C) {x y : ℂ} (hx : x ∉ C) (hy : y ∉ C) (hxy : y ∉ connectedComponentIn Cᶜ x) : frontier (connectedComponentIn Cᶜ x) = C

The frontier of a complementary component of a Jordan curve is the whole curve, provided the curve separates the plane: if C separates x from y, the component of Cᶜ containing x has frontier C.

theorem TauCeti.IsJordanCurve.disjoint_of_isOpen_of_subset_filledHull {C U : Set ℂ} (h : IsJordanCurve C) (hU : IsOpen U) (hUC : U ⊆ filledHull C) : Disjoint U C

An open set in the filled hull of a Jordan curve misses the curve. If U is open and contained in filledHull C for a Jordan curve C ⊆ ℂ, then U does not meet C.