Bounded complementary components in the one-point compactification

For a closed set in a proper locally connected metric space, the closure of a bounded complementary component in the one-point compactification adds only points of the closed set. Consequently a path avoiding the closed set cannot leave such a component, even through infinity.

Main results

• TauCeti.closure_image_coe_connectedComponentIn_subset describes that closure.
• TauCeti.not_joinedIn_compl_image_coe separates the component from every other point by paths.

theorem TauCeti.closure_image_coe_connectedComponentIn_subset {E : Type u_1} [MetricSpace E] [ProperSpace E] [LocallyConnectedSpace E] {K : Set E} (hK : IsClosed K) {x : E} (hx : x ∈ filledHull K) : closure (OnePoint.some '' connectedComponentIn Kᶜ x) ⊆ OnePoint.some '' (connectedComponentIn Kᶜ x ∪ K)

In the one-point compactification, the closure of a bounded component of the complement of a closed set K adds only points of K.

theorem TauCeti.not_joinedIn_compl_image_coe {E : Type u_1} [MetricSpace E] [ProperSpace E] [LocallyConnectedSpace E] {K : Set E} (hK : IsClosed K) {x : E} (hx : x ∈ filledHull K \ K) {w : OnePoint E} (hw : w ∉ OnePoint.some '' connectedComponentIn Kᶜ x) : ¬JoinedIn (OnePoint.some '' K)ᶜ (↑x) w

A point of the one-point compactification outside the image of a bounded complementary component of a closed set K cannot be joined to it by a path avoiding the image of K.