Commit 2024-10-01 17:04 0d57a343

View on Github →

feat(Topology/KrullDimension): add invariance under homeomorphism theorem and auxiliary lemmas (#17175) Added some lemmas about the topological Krull dimension

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Function.Injective.image_strictMono

Modified Mathlib/Topology/KrullDimension.lean

added theorem ClosedEmbedding.topologicalKrullDim_le

added def IrreducibleCloseds.map

added theorem IrreducibleCloseds.map_strictMono

added theorem IsHomeomorph.topologicalKrullDim_eq