isClopen

Mathlib.Topology.Sets.Closeds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Clopens.isClopen

English

For a clopen s, the underlying set is clopen: IsClopen (s:Set α).

Русский

Для clopen s соответствующее множество является открытым и замкнутым: IsClopen (s:Set α).

LaTeX

$$$ IsClopen\\big((s : Set\\,\\alpha)\\big) $$$

Lean4

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

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

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

Разделы

Аффилиация

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