noetherian top. space

Stream: Is there code for X?

[Reid Barton]

Do we have a definition of Noetherian topological spaces? And the dimension of a closed subset?

[Johan Commelin]

src/topology/noetherian_space.lean looks promising

[Johan Commelin]

But no dimension theory

[Reid Barton]

Aha, these didn't come up in the mathlib docs search because they are in a namespace and therefore much longer names than the ring theory ones

[Junyan Xu]

defining dimension should be straightforward from docs#set.chain_height (recently merged)