closed

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.RelCWComplex.Subcomplex.closed

English

For any E ∈ Subcomplex C, the underlying set (E : Set X) is closed.

Русский

Для любого E ∈ Subcomplex C множество (E : Set X) замкнуто.

LaTeX

$$$$IsClosed\left( E : Set X \right)$$$$

Lean4

theorem closed (E : Subcomplex C) : IsClosed (E : Set X) :=
  E.closed'

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

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

Разделы

Аффилиация

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