matrix

Mathlib.Topology.Instances.Matrix

URI: https://scilib.ai/kg/mathlib#IsCompact.matrix

← MathLib Explorer

English

If S is compact in R, then S.matrix is compact in M_{m,n}(R).

Русский

Если S компактно в R, то S.matrix компактно в M_{m,n}(R).

LaTeX

$$$\text{IsCompact}(S) \Rightarrow \text{IsCompact}(S.\mathrm{matrix})$$$

Lean4

theorem matrix [TopologicalSpace R] {S : Set R} (hS : IsCompact S) : IsCompact (S.matrix : Set (Matrix m n R)) :=
  isCompact_pi_infinite fun _ => isCompact_pi_infinite fun _ => hS

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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