isPathConnected_compl_singleton_of_one_lt_rank

English

Complement of a point is path-connected in higher dimensions.

Русский

Дополнение точки является path-connected в больших размерностях.

LaTeX

$$$\\text{IsPathConnected }({x})^{c}$ for dimension > 1$$

Lean4

/-- In a real vector space of dimension `> 1`, the complement of any singleton is path-connected. -/
theorem isPathConnected_compl_singleton_of_one_lt_rank (h : 1 < Module.rank ℝ E) (x : E) : IsPathConnected { x }ᶜ :=
  Set.Countable.isPathConnected_compl_of_one_lt_rank h (countable_singleton x)

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