English
Let F be a real topological vector space and E a subspace. If the codimension of E in F is greater than one (i.e., rank(F/E) > 1), then F \\ E is connected; equivalently, for any x ∈ F not in E, the connected component of x in F \\ E equals F \\ E.
Русский
Пусть F — вещественное топологическое векторное пространство, E — подпространство. Пусть кодимENSION(E in F) больше единицы, то F \ E связно; эквивалентно: для любого x ∈ F \ E связная компонента x в F \ E совпадает с F \ E.
LaTeX
$$$1 < \\operatorname{rank}_{\\mathbb{R}} \\big(F / E\\big) \\;\\Rightarrow\\; \\forall x \\in F \\setminus E,\\; \\operatorname{connectedComponentIn}((E : \\mathrm{Set} F)^{c})\\, x = (E : \\mathrm{Set} F)^{c}.$$$
Lean4
theorem connectedComponentIn_eq_self_of_one_lt_codim (E : Submodule ℝ F) (hcodim : 1 < Module.rank ℝ (F ⧸ E)) {x : F}
(hx : x ∉ E) : connectedComponentIn ((E : Set F)ᶜ) x = (E : Set F)ᶜ :=
(isConnected_compl_of_one_lt_codim hcodim).2.connectedComponentIn hx
