Commit 2025-02-03 07:17 ec5b3790
View on Github →refactor(Topology/Constructible): use QuasiSeparatedSpace
(#21325)
A few lemmas took assumptions of the formIsTopologicalBasis (range b)
+ ∀ i j, IsCompact (b i ∩ b j)
. But this is equivalent to the more natural set of assumptions IsTopologicalBasis (range b)
+ ∀ i, IsCompact (b i)
+ QuasiSeparatedSpace X
.
Also link to Stacks 0069.