Commit 2025-11-03 14:11 3881a2b2

View on Github →

feat(Topology/KrullDimension): add subspace dimension inequality (#29728) This PR proves that subspaces have Krull dimension at most that of the ambient space: dim(Y) ≤ dim(X) for Y ⊆ X (theorem topologicalKrullDim_subspace_le). Supporting results about IrreducibleCloseds were refactored and moved from KrullDimension.lean to Closeds.lean for better modularity. Note: Some code/documentation generated with AI assistance (Gemini).

Estimated changes

Modified Mathlib/Topology/KrullDimension.lean

deleted def IrreducibleCloseds.map

deleted theorem IrreducibleCloseds.map_strictMono

deleted theorem IsClosedEmbedding.topologicalKrullDim_le

added theorem IsInducing.topologicalKrullDim_le

added theorem topologicalKrullDim_subspace_le

Modified Mathlib/Topology/Sets/Closeds.lean

added theorem TopologicalSpace.IrreducibleCloseds.coe_map

added def TopologicalSpace.IrreducibleCloseds.map

added theorem TopologicalSpace.IrreducibleCloseds.map_injective_of_isInducing

added theorem TopologicalSpace.IrreducibleCloseds.map_mono

added theorem TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing