Category of Alexandrov-discrete topological spaces #

This defines AlexDisc, the category of Alexandrov-discrete topological spaces with continuous maps, and proves it's equivalent to the category of preorders.

    Auxiliary typeclass to define the category of Alexandrov-discrete spaces. Do not use this directly. Use AlexandrovDiscrete instead.

      def AlexDisc :
      Type (u_1 + 1)

      The category of Alexandrov-discrete spaces.

      Instances For

        Construct a bundled AlexDisc from the underlying topological space.

        Instances For
          theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
          ↑(AlexDisc.of α) = α
          theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
          def {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
          α β

          Constructs an equivalence between preorders from an order isomorphism between them.

          Instances For
            theorem alexDiscEquivPreord_inverse_map :
            ∀ {X Y : Preord} (f : X →o Y), f = f

            Sends a topological space to its specialisation order.

            Instances For