isClosed_ideal — Mathlib

English

In a Noetherian topological ring that is compact and T2, every ideal is closed.

Русский

В топологическом кольце Ноутерова типа компактности и T2 каждый идеал замкнут.

LaTeX

$$$I \text{ is closed in } R$ for any ideal I in a Noetherian ring under given conditions$$

Lean4

instance (priority := low) isClosed_ideal {R : Type*} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [IsNoetherianRing R] [CompactSpace R] [T2Space R] (I : Ideal R) : IsClosed (X := R) I :=
  (Ideal.isCompact_of_fg (IsNoetherian.noetherian I)).isClosed

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