instCompactSpaceElemCoeCompacts — Mathlib

English

There is a canonical compact space structure on the set of compacts; compatibility with the ambient space X is ensured.

Русский

Существует каноническая компактая структура на множестве компактов; совместимость с исходным пространством обеспечивается.

LaTeX

$$$\text{CompactSpace}(\mathrm{Compacts}(X))$$$

Lean4

instance {X : Type*} [TopologicalSpace X] (K : TopologicalSpace.Compacts X) : CompactSpace (K : Set X) :=
  TopologicalSpace.Compacts.instCompactSpaceSubtypeMem ..

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