compl

Mathlib.Topology.Sets.Closeds

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

English

The complement of a closed set is an open set.

Русский

complément замкнутого множества является открытым множеством.

LaTeX

$$$\mathrm{compl}(s) = s^{c} \in \mathrm{Opens}(\alpha).$$$

Lean4

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

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

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

Разделы

Аффилиация

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