This file defines a type synonym for a topological space considered with its specialisation order.
Type synonym for a topological space considered with its specialisation order.
toEquiv is the "identity" function to the Specialization of a type.
ofEquiv is the identity function from the Specialization of a type.
A recursor for Specialization. Use as induction x using Specialization.rec.
induction x using Specialization.rec
A continuous map between topological spaces induces a monotone map between their specialization
A preorder is isomorphic to the specialisation order of its upper set topology.
An Alexandrov-discrete space is isomorphic to the upper set topology of its specialisation
Sends a topological space to its specialisation order.