univ — Mathlib

English

If X is a completely metrizable space, then the whole universe (univ) viewed as a subset is completely metrizable.

Русский

Если пространство X полностью метризуемо, то вся вселенная (univ) как множество также полностью метризуема.

LaTeX

$$$[TopologicalSpace X][IsCompletelyMetrizableSpace X]\\Rightarrow IsCompletelyMetrizableSpace (univ : Set X)$$$

Lean4

instance univ [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : IsCompletelyMetrizableSpace (univ : Set X) :=
  isClosed_univ.isCompletelyMetrizableSpace

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