Commit 2023-09-15 17:12 481b5fc5

View on Github →

feat: Equivalence between Alexandrov-discrete spaces and preorders (#6989) Construct the category equivalence between Alexandrov-discrete spaces and preorders

Estimated changes

Modified Mathlib/Topology/Order/Category/AlexDisc.lean

added def alexDiscEquivPreord

Modified Mathlib/Topology/Specialization.lean

added theorem Specialization.isOpen_toEquiv_preimage

added theorem Specialization.isUpperSet_ofEquiv_preimage

added def homeoWithUpperSetTopologyorderIso

added def orderIsoSpecializationWithUpperSetTopology

added def topToPreord