of_isClosedEmbedding — Mathlib

English

If Y is prespectral and f : X → Y is a closed embedding, then X is prespectral.

Русский

Если Y prespectral и f: X → Y — закрытое вложение, то X prespectral.

LaTeX

$$$[\\mathrm{PrespectralSpace}(Y)] \\land \\mathrm{IsClosedEmbedding}(f) \\Rightarrow \\mathrm{PrespectralSpace}(X)$$$

Lean4

theorem of_isClosedEmbedding [PrespectralSpace Y] (f : X → Y) (hf : IsClosedEmbedding f) : PrespectralSpace X :=
  .of_isInducing f hf.isInducing hf.isProperMap.isSpectralMap

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