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.
• isPathConnected_compl_of_one_lt_codim shows that the complement of a subspace of codimension > 1 is path-connected.

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 : s.Countable) :

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 : s.Countable) :

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 any 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.

theorem isPathConnected_compl_of_one_lt_codim {F : Type u_1} [] [] [] [] {E : } (hcodim : 1 < Module.rank (F E)) :

Let E be a linear subspace in a real vector space. If E has codimension at least two, its complement is path-connected.

theorem isConnected_compl_of_one_lt_codim {F : Type u_1} [] [] [] [] {E : } (hcodim : 1 < Module.rank (F E)) :

Let E be a linear subspace in a real vector space. If E has codimension at least two, its complement is connected.

theorem Submodule.connectedComponentIn_eq_self_of_one_lt_codim {F : Type u_1} [] [] [] [] (E : ) (hcodim : 1 < Module.rank (F E)) {x : F} (hx : xE) :
= (E)