The Jordan curve theorem: the inside of a Jordan curve is connected

A Jordan curve C ⊆ ℂ separates the plane (TauCeti.IsJordanCurve.not_isPreconnected_compl), so its complement has a bounded component, and every complementary component has the whole curve as its frontier (TauCeti.IsJordanCurve.frontier_connectedComponentIn). This file proves the remaining half of the Jordan curve theorem: there is only one bounded component. So the inside filledHull C \ C of the curve is a single component of Cᶜ, hence open, bounded and connected with frontier C, and Cᶜ has exactly two components, the inside and the unbounded outside.

The count comes from the Riemann sphere, where the Jordan–Brouwer separation theorem gives exactly two path components for the complement of the image J of C (TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint). The image of a bounded component D of Cᶜ is open in the sphere, and its closure there is the image of the compact set closure D ⊆ D ∪ C, so it is clopen in Jᶜ and misses the point at infinity. Hence the images of two different bounded components and the point at infinity would lie in three different path components of Jᶜ.

Main results

• TauCeti.IsJordanCurve.mem_connectedComponentIn_of_mem_filledHull_sdiff — two points inside a Jordan curve lie in the same component of its complement.
• TauCeti.IsJordanCurve.filledHull_sdiff_eq_connectedComponentIn — the inside of a Jordan curve is the component of its complement containing any of its points.
• TauCeti.IsJordanCurve.isConnected_filledHull_sdiff — the inside of a Jordan curve is connected.
• TauCeti.IsJordanCurve.frontier_filledHull_sdiff — the frontier of the inside of a Jordan curve is the curve.
• TauCeti.IsJordanCurve.frontier_filledHull — the curve is also the frontier of its filled hull, hence of its outside.
• TauCeti.IsJordanCurve.interior_filledHull, TauCeti.IsJordanCurve.closure_filledHull_sdiff and TauCeti.IsJordanCurve.closure_compl_filledHull — the inside is the interior of the filled hull, whose closure it is, and the closure of the outside is the complement of the inside.
• TauCeti.IsJordanCurve.frontier_insert_zero_image_inv_sub_compl_filledHull — the outside, inverted about a point p of the inside by z ↦ (z - p)⁻¹ and completed by 0, the image of infinity, is bounded by the inverted curve.
• TauCeti.IsJordanCurve.connectedComponentIn_eq_filledHull_sdiff_or_compl — every complementary component of a Jordan curve is its inside or its outside. The outside is connected for any bounded set, by TauCeti.isConnected_compl_filledHull.
• TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two — the Jordan curve theorem: the complement of a Jordan curve in the plane has exactly two connected components.

References

• A. Hatcher, Algebraic Topology, Section 2.B, Corollary 2B.2.
• J. R. Munkres, Topology, §61–63.

theorem TauCeti.IsJordanCurve.mem_connectedComponentIn_of_mem_filledHull_sdiff {C : Set ℂ} (hC : IsJordanCurve C) {x y : ℂ} (hx : x ∈ filledHull C \ C) (hy : y ∈ filledHull C \ C) : y ∈ connectedComponentIn Cᶜ x

A Jordan curve has only one bounded complementary component. Two points of the inside filledHull C \ C of a Jordan curve C ⊆ ℂ lie in the same component of Cᶜ.

theorem TauCeti.IsJordanCurve.filledHull_sdiff_eq_connectedComponentIn {C : Set ℂ} (hC : IsJordanCurve C) {x : ℂ} (hx : x ∈ filledHull C \ C) : filledHull C \ C = connectedComponentIn Cᶜ x

The inside of a Jordan curve is a single complementary component. For a Jordan curve C ⊆ ℂ and any point x of its inside, filledHull C \ C is the component of Cᶜ containing x.

theorem TauCeti.IsJordanCurve.isConnected_filledHull_sdiff {C : Set ℂ} (hC : IsJordanCurve C) : IsConnected (filledHull C \ C)

The inside of a Jordan curve is connected.

theorem TauCeti.IsJordanCurve.frontier_filledHull_sdiff {C : Set ℂ} (hC : IsJordanCurve C) : frontier (filledHull C \ C) = C

A Jordan curve bounds its inside. The frontier of the inside filledHull C \ C of a Jordan curve C ⊆ ℂ is C.

@[simp]

theorem TauCeti.IsJordanCurve.frontier_filledHull {C : Set ℂ} (hC : IsJordanCurve C) : frontier (filledHull C) = C

A Jordan curve bounds its filled hull. The frontier of filledHull C for a Jordan curve C ⊆ ℂ is C; equivalently (frontier_compl) the curve is the frontier of its outside (filledHull C)ᶜ.

@[simp]

theorem TauCeti.IsJordanCurve.interior_filledHull {C : Set ℂ} (hC : IsJordanCurve C) : interior (filledHull C) = filledHull C \ C

The interior of the filled hull of a Jordan curve C ⊆ ℂ is its inside filledHull C \ C.

@[simp]

theorem TauCeti.IsJordanCurve.closure_filledHull_sdiff {C : Set ℂ} (hC : IsJordanCurve C) : closure (filledHull C \ C) = filledHull C

The closure of the inside filledHull C \ C of a Jordan curve C ⊆ ℂ is its filled hull.

theorem TauCeti.IsJordanCurve.closure_compl_filledHull {C : Set ℂ} (hC : IsJordanCurve C) : closure (filledHull C)ᶜ = (filledHull C \ C)ᶜ

The closure of the outside (filledHull C)ᶜ of a Jordan curve C ⊆ ℂ is the complement of its inside.

theorem TauCeti.IsJordanCurve.notMem_closure_compl_filledHull {C : Set ℂ} (hC : IsJordanCurve C) {p : ℂ} (hp : p ∈ filledHull C \ C) : p ∉ closure (filledHull C)ᶜ

A point of the inside of a Jordan curve C ⊆ ℂ lies off the closure of its outside.

theorem TauCeti.IsJordanCurve.frontier_insert_zero_image_inv_sub_compl_filledHull {C : Set ℂ} (hC : IsJordanCurve C) {p : ℂ} (hp : p ∈ filledHull C \ C) : frontier (insert 0 ((fun (z : ℂ) => (z - p)⁻¹) '' (filledHull C)ᶜ)) = (fun (z : ℂ) => (z - p)⁻¹) '' C

The inverted outside of a Jordan curve is bounded by the inverted curve. Inverting the outside (filledHull C)ᶜ of a Jordan curve C ⊆ ℂ about a point p of its inside and adding 0, the image of infinity, gives an open set whose frontier is the image of C.

theorem TauCeti.IsJordanCurve.connectedComponentIn_eq_filledHull_sdiff_or_compl {C : Set ℂ} (hC : IsJordanCurve C) {x : ℂ} (hx : x ∉ C) : connectedComponentIn Cᶜ x = filledHull C \ C ∨ connectedComponentIn Cᶜ x = (filledHull C)ᶜ

Every complementary component of a Jordan curve C ⊆ ℂ is either its inside filledHull C \ C or its outside (filledHull C)ᶜ.

theorem TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two {C : Set ℂ} (hC : IsJordanCurve C) : Nat.card (ConnectedComponents ↑Cᶜ) = 2

The Jordan curve theorem. The complement of a Jordan curve in the plane has exactly two connected components: by TauCeti.IsJordanCurve.connectedComponentIn_eq_filledHull_sdiff_or_compl they are its inside filledHull C \ C and its unbounded outside (filledHull C)ᶜ.