univ_perfect

Mathlib.Topology.Perfect

URI: https://scilib.ai/kg/mathlib#PerfectSpace.univ_perfect

English

In a PerfectSpace, the entire space considered as a set is perfect.

Русский

В совершенном пространстве всё пространство как множество совершенно.

LaTeX

$$$\text{Perfect}(\mathrm{Set.univ})$ under [PerfectSpace].$$

Lean4

theorem univ_perfect [PerfectSpace α] : Perfect (Set.univ : Set α) :=
  ⟨isClosed_univ, PerfectSpace.univ_preperfect⟩

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

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

Разделы

Аффилиация

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