2023-09-07 05:09
Mathlib/Topology/NoetherianSpace.lean
feat : Stacks: Lemma 0052 (3) irreducible component of noetherian space contains a nonempty open subset (#6881) …
Added TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent