English
Topological Krull dimension is invariant under homeomorphisms.
Русский
Топологическая размерность Крull инвариантна относительно гомеоморфизмов.
LaTeX
$$$\operatorname{topologicalKrullDim}(X) = \operatorname{topologicalKrullDim}(Y) \quad \text{if } X \cong Y$$$
Lean4
/-- The topological Krull dimension is invariant under homeomorphisms -/
theorem topologicalKrullDim_eq (f : X → Y) (h : IsHomeomorph f) : topologicalKrullDim X = topologicalKrullDim Y :=
have fwd : topologicalKrullDim X ≤ topologicalKrullDim Y :=
IsClosedEmbedding.topologicalKrullDim_le f h.isClosedEmbedding
have bwd : topologicalKrullDim Y ≤ topologicalKrullDim X :=
IsClosedEmbedding.topologicalKrullDim_le (h.homeomorph f).symm (h.homeomorph f).symm.isClosedEmbedding
le_antisymm fwd bwd
