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

Modified Mathlib/Topology/Constructible.lean

Modified Mathlib/Topology/QuasiSeparated.lean

added theorem IsCompact.inter_of_isOpen

modified theorem IsQuasiSeparated.of_quasiSeparatedSpace

modified theorem QuasiSeparatedSpace.of_isOpenEmbedding

added theorem QuasiSeparatedSpace.of_isTopologicalBasis