Theorems · Theorem · general topology

isConnected_compl_singleton_of_one_lt_rank

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ (x : E), IsConnected {x}ᶜ

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

Defined in

Mathlib.Analysis.Normed.Module.Connected

Cited by

2 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleTopologicalSpaceContinuousAddContinuousSMul