isPathConnected_compl_of_one_lt_codim

English

Higher-dimensional spheres are path-connected for nonnegative radius.

Русский

Сферы в пространствах большей размерности путь-соединены для r ≥ 0.

LaTeX

$$$\\text{IsPathConnected}(\\text{sphere}(x,r))$ for $1<\\dim E$ and $r\\ge 0$$$

Lean4

/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is path-connected. -/
theorem isPathConnected_compl_of_one_lt_codim {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) :
    IsPathConnected (Eᶜ : Set F) := by
  rcases E.exists_isCompl with ⟨E', hE'⟩
  refine
    isPathConnected_compl_of_isPathConnected_compl_zero hE'.symm (isPathConnected_compl_singleton_of_one_lt_rank ?_ 0)
  rwa [← (E.quotientEquivOfIsCompl E' hE').rank_eq]

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