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:

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

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

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

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

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) :

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) :

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

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