instT0Space

Mathlib.Topology.UniformSpace.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.instT0Space

English

If 𝕜 is a T0Space, then the matrix space Matrix m n 𝕜 is also a T0Space.

Русский

Если 𝕜 является T0-пространством, то пространство матриц Matrix m n 𝕜 тоже является T0.

LaTeX

$$$[T0Space 𝕜] \Rightarrow T0Space (Matrix m n 𝕜)$$$

Lean4

instance [T0Space 𝕜] : T0Space (Matrix m n 𝕜) :=
  inferInstanceAs (T0Space (m → n → 𝕜))

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

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

Разделы

Аффилиация

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