isCompact_of_fg

Mathlib.Topology.Algebra.Module.Compact

URI: https://scilib.ai/kg/mathlib#Ideal.isCompact_of_fg

English

The toSubmodule of the iSup equals the closure of the iSup of the submodules.

Русский

toSubmodule(⨆ i, f i) = closure(⨆ i, (f i).toSubmodule).closure

LaTeX

$$$toSubmodule(\iSup f) = (\iSup (f i).toSubmodule).closure$$$

Lean4

theorem isCompact_of_fg [IsTopologicalSemiring R] [CompactSpace R] {I : Ideal R} (hI : I.FG) : IsCompact (X := R) I :=
  Submodule.isCompact_of_fg hI

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

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

Разделы

Аффилиация

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