Commit 2023-02-13 21:12 54d77d95

View on Github →

feat port Topology.QuasiSeparated (#2261)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/QuasiSeparated.lean

added theorem IsQuasiSeparated.image_of_embedding

added theorem IsQuasiSeparated.of_quasiSeparatedSpace

added theorem IsQuasiSeparated.of_subset

added def IsQuasiSeparated

added theorem OpenEmbedding.isQuasiSeparated_iff

added theorem QuasiSeparatedSpace.of_openEmbedding

added theorem isQuasiSeparated_iff_quasiSeparatedSpace

added theorem isQuasiSeparated_univ

added theorem isQuasiSeparated_univ_iff