compactSpace_iff_quasiCompact — Mathlib

English

For any scheme X, X is compact if and only if the unique map from the terminal scheme to X is quasi-compact.

Русский

Для схемы X имеет место равносильность: X компактна тогда и только тогда, когда единственный морфизм от терминального схемы к X квази-компактен.

LaTeX

$$$\\CompactSpace X \\iff \\QuasiCompact (\\mathrm{terminal.from}\\ X)$$$

Lean4

theorem compactSpace_iff_quasiCompact (X : Scheme) : CompactSpace X ↔ QuasiCompact (terminal.from X) := by
  rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

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