isClopen

Mathlib.Topology.Sets.Order

URI: https://scilib.ai/kg/mathlib#ClopenUpperSet.isClopen

English

A clopen upper set is a clopen subset of the space.

Русский

Клопное верхнее множество является открытым и закрытым подмножеством пространства.

LaTeX

$$$\\\\text{isClopen}(s) =\\\\text{IsClopen}(s : Set\\\\alpha).$$$

Lean4

theorem isClopen (s : ClopenUpperSet α) : IsClopen (s : Set α) :=
  s.isClopen'

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

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

Разделы

Аффилиация

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