instCompleteSpace — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance [CompleteSpace 𝕜] : CompleteSpace (Matrix m n 𝕜) :=
  (by infer_instance : CompleteSpace (m → n → 𝕜))

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