isOpen_singleton_true

Mathlib.Topology.Order

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

English

In the Sierpinski space, the singleton {True} is open.

Русский

В пространстве Сирпенски единичное множество {True} является открытым.

LaTeX

$$$\\text{IsOpen}({\\text{True}}).$$$

Lean4

@[simp]
theorem isOpen_singleton_true : IsOpen ({ True } : Set Prop) :=
  TopologicalSpace.GenerateOpen.basic _ (mem_singleton _)

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

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

Разделы

Аффилиация

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