Closed equivalence relation with an open quotient map (source code)

= Closed equivalence relation with an open quotient map

If an <equivalence relation> is closed in a space's square and the <quotient map> is open, the <quotient> is <Hausdorff>. An inequivalent pair has an open rectangle avoiding the relation. The two factor <images> are open <quotient> neighborhoods and are disjoint, since an <intersection> would give equivalent representatives in that rectangle. Conversely, a <Hausdorff> <quotient> always has a closed <equivalence relation> by pulling back its closed diagonal.