isTotallyDisconnected_singleton

Mathlib.Topology.Connected.TotallyDisconnected

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

English

A singleton set is totally disconnected.

Русский

Одиночное множество — totally disconnected.

LaTeX

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

Lean4

theorem isTotallyDisconnected_singleton {x} : IsTotallyDisconnected ({ x } : Set α) := fun _ ht _ =>
  subsingleton_singleton.anti ht

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

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

Разделы

Аффилиация

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