isTotallySeparated_singleton

Mathlib.Topology.Connected.TotallyDisconnected

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

← MathLib Explorer

English

Singleton sets are totally separated.

Русский

Единственные множества полностью разделимы.

LaTeX

$$IsTotallySeparated({x} : Set α)$$

Lean4

theorem isTotallySeparated_singleton {x} : IsTotallySeparated ({ x } : Set α) := fun _ hp _ hq hpq =>
  (hpq <| (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim

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

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

Разделы

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

Аффилиация

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