Unification of Graphs and Relations in Mizar

Abstract

A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system [2], based on the formalization of graphs in [6] and relations in [11], [12]. Notably, a new definition of createGraph will be given, taking only a non empty set V and a binary relation E ⊆ V × V to create a (di)graph without parallel edges, which will provide to be very useful in future articles.