isOpen_compl_iff

Mathlib.Topology.Basic

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

English

An open set’s complement is closed, and vice versa.

Русский

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

LaTeX

$$$IsOpen s^c \iff IsClosed s$$$

Lean4

@[simp]
theorem isOpen_compl_iff : IsOpen sᶜ ↔ IsClosed s :=
  ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩

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

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

Разделы

Аффилиация

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