compactSpace_of_isAffine — Mathlib

English

If X is an affine scheme, then the underlying topological space of X is compact.

Русский

Если X является афинной схемой, то топологическое пространство X является компактным.

LaTeX

$$$\operatorname{CompactSpace}(X)$$$

Lean4

instance (priority := 100) _root_.AlgebraicGeometry.Scheme.compactSpace_of_isAffine (X : Scheme) [IsAffine X] :
    CompactSpace X :=
  ⟨(isAffineOpen_top X).isCompact⟩

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