Commit 2024-07-04 14:02 f7295838

View on Github →

feat(Topology/KrullDimension.lean): Krull dimension of a topological space (#13178) Define the Krull dimension of a topological space: the Krull dimension of a topological space is the supremum of lengths of chains of closed irreducible sets.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Created Mathlib/Topology/KrullDimension.lean

Modified Mathlib/Topology/Sets/Closeds.lean

added def TopologicalSpace.IrreducibleCloseds.Simps.coe

added theorem TopologicalSpace.IrreducibleCloseds.coe_mk

added def TopologicalSpace.IrreducibleCloseds.equivSubtype'

added def TopologicalSpace.IrreducibleCloseds.equivSubtype

added theorem TopologicalSpace.IrreducibleCloseds.isClosed

added theorem TopologicalSpace.IrreducibleCloseds.isIrreducible

added theorem TopologicalSpace.IrreducibleCloseds.mem_singleton

added def TopologicalSpace.IrreducibleCloseds.orderIsoSubtype'

added def TopologicalSpace.IrreducibleCloseds.orderIsoSubtype

added def TopologicalSpace.IrreducibleCloseds.singleton

added structure TopologicalSpace.IrreducibleCloseds

Modified Mathlib/Topology/Sober.lean