isConnected_compl_singleton_of_one_lt_rank

Mathlib.Analysis.NormedSpace.Connected

URI: https://scilib.ai/kg/mathlib#isConnected_compl_singleton_of_one_lt_rank

← MathLib Explorer

English

Complement of a single point is connected.

Русский

Дополнение точки связано.

LaTeX

$$$\\text{IsConnected }(\\{x\\}^{c})$ for dim > 1$$

Lean4

/-- In a real vector space of dimension `> 1`, the complement of a singleton is connected. -/
theorem isConnected_compl_singleton_of_one_lt_rank (h : 1 < Module.rank ℝ E) (x : E) : IsConnected { x }ᶜ :=
  (isPathConnected_compl_singleton_of_one_lt_rank h x).isConnected

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru