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.

Estimated changes