# Documentation

Mathlib.Analysis.NormedSpace.Connected

# 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} [] [] [] [] [] (h : 1 < ) {s : Set E} (hs : ) :

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} [] [] [] [] [] (h : 1 < ) {s : Set E} (hs : ) :

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} [] [] [] [] [] (h : 1 < ) (x : E) :

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} [] [] [] [] [] (h : 1 < ) (x : E) :

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

theorem isPathConnected_sphere {E : Type u_1} [] (h : 1 < ) (x : E) {r : } (hr : 0 r) :

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

theorem isConnected_sphere {E : Type u_1} [] (h : 1 < ) (x : E) {r : } (hr : 0 r) :

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

theorem isPreconnected_sphere {E : Type u_1} [] (h : 1 < ) (x : E) (r : ) :

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