Theorem TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent

Modification history

2025-12-11 22:59
Mathlib/Topology/NoetherianSpace.lean
chore: use `Set.Nonempty` everywhere (#32697)
Added TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponentView on Github →