instCompactSpaceQuotientIdeal

Mathlib.Topology.Algebra.Ring.Ideal

URI: https://scilib.ai/kg/mathlib#instCompactSpaceQuotientIdeal

English

If R is compact and N is an ideal, then the quotient R/N is compact.

Русский

Если R компактно, а N — идеал, то фактор-кольцо R/N компактно.

LaTeX

$$$ [CompactSpace R] \Rightarrow CompactSpace(R / N) $$$

Lean4

instance [CompactSpace R] : CompactSpace (R ⧸ N) :=
  Quotient.compactSpace

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

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

Разделы

Аффилиация

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