Connectedness of punctured balls

In an affine space over a real seminormed space of dimension greater than one, removing the centre from an open ball of positive radius leaves a path-connected set. This is the local form of Mathlib's isPathConnected_compl_singleton_of_one_lt_rank, to which it reduces through the homeomorphism OpenPartialHomeomorph.univBall of the model vector space onto the ball, sending 0 to the centre. It is the local input for showing that removing a discrete set from a connected manifold of dimension greater than one keeps it connected: through a partial homeomorphism to the affine space, every point of its source has arbitrarily small neighbourhoods whose punctured versions are connected.

Main declarations

• TauCeti.isPathConnected_ball_sdiff_singleton, TauCeti.isConnected_ball_sdiff_singleton: a punctured open ball is path connected, hence connected.
• TauCeti.exists_mem_nhds_subset_isConnected_sdiff_singleton_of_mem_source: every point in the source of a partial homeomorphism to the affine space has arbitrarily small neighbourhoods whose punctured versions are connected.

theorem TauCeti.isPathConnected_ball_sdiff_singleton {E : Type u_1} {P : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P] (h : 1 < Module.rank ℝ E) (x : P) {r : ℝ} (hr : 0 < r) : IsPathConnected (Metric.ball x r \ {x})

In an affine space over a real seminormed space of dimension greater than one, an open ball of positive radius with its centre removed is path connected.

theorem TauCeti.isConnected_ball_sdiff_singleton {E : Type u_1} {P : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P] (h : 1 < Module.rank ℝ E) (x : P) {r : ℝ} (hr : 0 < r) : IsConnected (Metric.ball x r \ {x})

In an affine space over a real seminormed space of dimension greater than one, an open ball of positive radius with its centre removed is connected.

theorem TauCeti.exists_mem_nhds_subset_isConnected_sdiff_singleton_of_mem_source {E : Type u_1} {P : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P] {X : Type u_3} [TopologicalSpace X] (h : 1 < Module.rank ℝ E) (φ : OpenPartialHomeomorph X P) {x : X} (hx : x ∈ φ.source) {U : Set X} (hU : U ∈ nhds x) : ∃ V ∈ nhds x, V ⊆ U ∧ IsConnected (V \ {x})

If P is an affine space over a real seminormed space of dimension greater than one, every point x in the source of a partial homeomorphism φ : X → P has arbitrarily small neighbourhoods V with V \ {x} connected.