isClosed_cl

Mathlib.Topology.Category.Compactum

URI: https://scilib.ai/kg/mathlib#Compactum.isClosed_cl

English

The closure of any set A in Compactum is closed.

Русский

Замкнутость замыкания любой множества A в Compactum.

LaTeX

$$$\\operatorname{IsClosed}(\\operatorname{cl}(A))$$$

Lean4

theorem isClosed_cl {X : Compactum} (A : Set X) : IsClosed (cl A) :=
  by
  rw [isClosed_iff]
  intro F hF
  exact cl_cl _ ⟨F, hF, rfl⟩

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

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

Разделы

Аффилиация

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