mathlib

64d86f7a - feat(topology/{subset_properties,separation}): closed subsets of compact t0 spaces contain a closed point (#6273)

feat(topology/{subset_properties,separation}): closed subsets of compact t0 spaces contain a closed point (#6273) This adds two statements. The first is that nonempty closed subsets of a compact space have a minimal nonempty closed subset, and the second is that when the space is additionally T0 then that minimal subset is a singleton. (This PR does not do this, but one can go on to show that there is functor from compact T0 spaces to T1 spaces by taking the set of closed points, and it preserves nonemptiness.)