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} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (h : 1 < Module.rank ℝ E) {s : Set E} (hs : s.Countable) : 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 : s.Countable) : 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 any 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 Metric.contractibleSpace_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : ContractibleSpace ↑(ball x r)

@[deprecated Metric.contractibleSpace_ball (since := "2026-02-02")]

theorem Metric.ball_contractible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : ContractibleSpace ↑(ball x r)

Alias of Metric.contractibleSpace_ball.

theorem Metric.contractibleSpace_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : ContractibleSpace ↑(eball x r)

@[deprecated Metric.contractibleSpace_eball (since := "2026-02-02")]

theorem Metric.eball_contractible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : ContractibleSpace ↑(eball x r)

Alias of Metric.contractibleSpace_eball.

theorem Metric.contractibleSpace_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 ≤ r) : ContractibleSpace ↑(closedBall x r)

instance Metric.contractibleSpace_closedEBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : ContractibleSpace ↑(closedEBall x r)

theorem Metric.isPathConnected_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : IsPathConnected (ball x r)

theorem Metric.isPathConnected_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : IsPathConnected (eball x r)

theorem Metric.isPathConnected_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 ≤ r) : IsPathConnected (closedBall x r)

theorem Metric.isPathConnected_closedEBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPathConnected (closedEBall x r)

theorem Metric.isPreconnected_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} : IsPreconnected (ball x r)

theorem Metric.isPreconnected_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPreconnected (eball x r)

theorem Metric.isPreconnected_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} : IsPreconnected (closedBall x r)

theorem Metric.isPreconnected_closedEBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPreconnected (closedEBall x r)

theorem Metric.isConnected_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 < r) : IsConnected (ball x r)

theorem Metric.isConnected_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : IsConnected (eball x r)

theorem Metric.isConnected_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ} (hr : 0 ≤ r) : IsConnected (closedBall x r)

theorem Metric.isConnected_closedEBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsConnected (closedEBall x r)

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.

theorem isPathConnected_compl_of_one_lt_codim {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) : IsPathConnected (↑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} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) : IsConnected (↑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} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (E : Submodule ℝ F) (hcodim : 1 < Module.rank ℝ (F ⧸ E)) {x : F} (hx : x ∉ E) : connectedComponentIn (↑E)ᶜ x = (↑E)ᶜ