compactSpace

Mathlib.Topology.Algebra.Module.Compact

URI: https://scilib.ai/kg/mathlib#Module.Finite.compactSpace

English

If R is compact and M is a finite R-module, then M is a compact space.

Русский

Если R компактно, и M — конечный модуль над R, тогда M компактно как пространство.

LaTeX

$$$\text{CompactSpace } M$$$

Lean4

theorem compactSpace [CompactSpace R] [Module.Finite R M] : CompactSpace M :=
  ⟨Submodule.isCompact_of_fg (Module.Finite.fg_top (R := R))⟩

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

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

Разделы

Аффилиация

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