not

Mathlib.Topology.Basic

URI: https://scilib.ai/kg/mathlib#IsClosed.not

English

If a set is closed, its complement is open.

Русский

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

LaTeX

$$$\operatorname{IsClosed}(\{x \mid p(x)\}) \Rightarrow \operatorname{IsOpen}(\{x \mid \lnot p(x)\})$$$

Lean4

theorem not : IsClosed {a | p a} → IsOpen {a | ¬p a} :=
  isOpen_compl_iff.mpr

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

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

Разделы

Аффилиация

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