topologicalKrullDim_le — Mathlib

English

If f is a closed embedding, then topologicalKrullDim(X) ≤ topologicalKrullDim(Y).

Русский

Если f — замкнутое вложение, то топологическая размерность Крull не возрастает: X ⟶ Y не хуже по размерности.

LaTeX

$$$ \operatorname{topologicalKrullDim}(X) \le \operatorname{topologicalKrullDim}(Y). $$$

Lean4

/-- If `f : X → Y` is a closed embedding, then the Krull dimension of `X` is less than or equal
to the Krull dimension of `Y`.
-/
theorem topologicalKrullDim_le (f : X → Y) (hf : IsClosedEmbedding f) : topologicalKrullDim X ≤ topologicalKrullDim Y :=
  krullDim_le_of_strictMono _ (IrreducibleCloseds.map_strictMono hf)

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