quasiCompact_iff_spectral — Mathlib

English

A morphism is quasi-compact if and only if its underlying continuous map on topological spaces is spectral.

Русский

Морфизм квази-компактен тогда и только тогда, когда соответствующее непрерывное отображение на топологическом уровне спектральна.

LaTeX

$$$\operatorname{QuasiCompact}(f) \iff IsSpectralMap(f.base)$$$

Lean4

theorem quasiCompact_iff_spectral : QuasiCompact f ↔ IsSpectralMap f.base :=
  ⟨fun ⟨h⟩ => ⟨by fun_prop, h⟩, fun h => ⟨h.2⟩⟩

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