isOpen

Mathlib.Topology.Clopen

URI: https://scilib.ai/kg/mathlib#IsClopen.isOpen

English

A subset is clopen if and only if it is both open and closed.

Русский

Множество является одновременно открытым и замкнутым тогда и только тогда, когда оно открыто и замкнуто.

LaTeX

$$$IsClopen\ s\iff (s\text{ is open }\land s\text{ is closed})$$$

Lean4

protected theorem isOpen (hs : IsClopen s) : IsOpen s :=
  hs.2

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

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

Разделы

Аффилиация

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