instUniformSpace

Mathlib.Topology.Instances.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.instUniformSpace

English

If R and M are complete, then tsze R M is complete.

Русский

Если R и M полные топологические пространства, то tsze R M также полное пространство.

LaTeX

$$$\\operatorname{CompleteSpace}(\\mathrm{tsze}(R,M))$$$

Lean4

instance instUniformSpace : UniformSpace (tsze R M)
    where
  toTopologicalSpace := instTopologicalSpace
  __ := instUniformSpaceProd

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

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

Разделы

Аффилиация

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