Theorems · Theorem · general topology

isConnected_compl_of_one_lt_codim

∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] {E : Submodule ℝ F}, 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.

Defined in

Mathlib.Analysis.Normed.Module.Connected

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul