singleton

Mathlib.Topology.Constructible

URI: https://scilib.ai/kg/mathlib#IsRetrocompact.singleton

English

Any singleton set is retrocompact.

Русский

Любное множество, состоящее из одного элемента, ретрокомпактно.

LaTeX

$$$\forall a:\; \{a\} \text{ retrocompact}$$$

Lean4

@[simp]
theorem singleton : IsRetrocompact { a } := fun _ _ _ ↦ Subsingleton.singleton_inter.isCompact

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

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

Разделы

Аффилиация

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