compl

Mathlib.Topology.Sets.Closeds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.compl

English

The complement of an open set is a closed set.

Русский

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

LaTeX

$$$\mathrm{compl}(O) = O^{c} \in \mathrm{Closeds}(\alpha).$$$

Lean4

/-- The complement of an open set as a closed set. -/
@[simps]
def compl (s : Opens α) : Closeds α :=
  ⟨sᶜ, s.2.isClosed_compl⟩

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

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

Разделы

Аффилиация

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