instSecondCountableTopology

Mathlib.Topology.MetricSpace.Polish

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.CompleteCopy.instSecondCountableTopology

English

CompleteCopy s is a T0 space (inherits T0 from its parent).

Русский

CompleteCopy s является T0-пространством.

LaTeX

$$$$\\text{T0Space}(CompleteCopy\,s).$$$$

Lean4

instance [SecondCountableTopology α] : SecondCountableTopology (CompleteCopy s) :=
  inferInstanceAs (SecondCountableTopology s)

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

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

Разделы

Аффилиация

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