feat(Topology/Spectral/ConstructibleTopology): if a topological space X is T0 and prespectral, then X is T2 in the constructible topology#40242

FMLJohn wants to merge 10 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

FMLJohn:spectralMap_propertiesFMLJohn/constructibleTop_T2:spectralMap_propertiesCopy head branch name to clipboard