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

Commits

Commits on Jun 3, 2026

Commits on Jun 4, 2026

Commits on Jun 5, 2026

Commits on Jun 7, 2026

Commits on Jun 12, 2026

Commits on Jun 13, 2026

Commits on Jun 22, 2026

Commits on Jul 8, 2026

Commits on Jul 16, 2026