Skip to content

feat(Topology/Spectral/ConstructibleTopology): the constructible topology on a compact quasi-separated space X equals the topology generated by the constructible subsets of X#40180

Open
FMLJohn wants to merge 33 commits into
leanprover-community:masterfrom
FMLJohn:constructibleTop_T2
Open

feat(Topology/Spectral/ConstructibleTopology): the constructible topology on a compact quasi-separated space X equals the topology generated by the constructible subsets of X#40180
FMLJohn wants to merge 33 commits into
leanprover-community:masterfrom
FMLJohn:constructibleTop_T2

Merge branch 'master' into constructibleTop_T2

b9eeed9
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jul 16, 2026 in 1m 21s