Connectedness of subsets of vector spaces

We show several results related to the (path)-connectedness of subsets of real vector spaces:

• Set.Countable.isPathConnected_compl_of_one_lt_rank asserts that the complement of a countable set is path-connected in a space of dimension > 1.
• isPathConnected_compl_singleton_of_one_lt_rank is the special case of the complement of a singleton.
• isPathConnected_sphere shows that any sphere is path-connected in dimension > 1.

Statements with connectedness instead of path-connectedness are also given.

theorem Set.Countable.isPathConnected_compl_of_one_lt_rank {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (h : 1 < Module.rank ℝ E) {s : Set E} (hs : Set.Countable s) : IsPathConnected sᶜ

In a real vector space of dimension > 1, the complement of any countable set is path connected.

theorem Set.Countable.isConnected_compl_of_one_lt_rank {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (h : 1 < Module.rank ℝ E) {s : Set E} (hs : Set.Countable s) : IsConnected sᶜ

In a real vector space of dimension > 1, the complement of any countable set is connected.

theorem isPathConnected_compl_singleton_of_one_lt_rank {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (h : 1 < Module.rank ℝ E) (x : E) : IsPathConnected {x}ᶜ

In a real vector space of dimension > 1, the complement of a singleton is path connected.

theorem isConnected_compl_singleton_of_one_lt_rank {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (h : 1 < Module.rank ℝ E) (x : E) : IsConnected {x}ᶜ

In a real vector space of dimension > 1, the complement of a singleton is connected.

theorem isPathConnected_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsPathConnected (Metric.sphere x r)

In a real vector space of dimension > 1, any sphere of nonnegative radius is path connected.

theorem isConnected_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsConnected (Metric.sphere x r)

In a real vector space of dimension > 1, any sphere of nonnegative radius is connected.

theorem isPreconnected_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.rank ℝ E) (x : E) (r : ℝ) : IsPreconnected (Metric.sphere x r)

In a real vector space of dimension > 1, any sphere is preconnected.