isConnected_compl_of_one_lt_codim

English

Complement of a high-codimension subspace is path-connected.

Русский

Дополнение подпространства с кодимером не ниже двух является path-connected.

LaTeX

$$$\\text{IsPathConnected} (E^{c} : Set F)$ under $\\text{codim}(E) \\ge 2$$$

Lean4

/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is connected. -/
theorem isConnected_compl_of_one_lt_codim {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) :
    IsConnected (Eᶜ : Set F) :=
  (isPathConnected_compl_of_one_lt_codim hcodim).isConnected

Похожие утверждения