@MISC{GLIB_014.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {About Graph Unions and Intersections},
  SECTION1 = {Sets of Graphs},
  SECTION2 = {Union of Graphs},
  SECTION3 = {Intersection of Graphs},
  DAY = {19},
  MONTH = {May},
  YEAR = {2020},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In this article the union and intersection of a set of graphs are 
  formalized in the Mizar system\cite{FourDecades}, based on the formalization 
  of graphs in \cite{GLIB_000.ABS}.},
  INTRODUCTION = {The union and intersection of two graphs are usually defined in any general graph theory 
  textbook, although there are small differences between the authors from time to time. For example, 
  Wilson \cite{SIMPLE} only allows two vertex- and edge-disjoint graphs to be united; his graph union 
  is usally known as the disjoint union\cite{MULTI,HANDBOOK} or sum\cite{HANDBOOK} of two graphs, 
  which will be formalized in in detail in another article. Bondy and Murty\cite{MULTI} as well as 
  Diestel\cite{DIEST} allow unions of two arbitary simple graphs, but labelled the vertices in the 
  graphical representation to avoid confusion. In both books it was silently assumed that edges between 
  the same vertices in both graphs are the same, thereby securing the union to be a simple graph again. 
  Wagner \cite{GERWAG}, while generalizing to the union and intersection of a family of graphs, 
  explicitly states that condition and previously adds the condition, that on the other side identical edges 
  in the graph family must have the same incident vertices. Naturally, in this paper union and intersection are 
  generalized to families of multidigraphs, i.e. the graphs of \cite{GLIB_000.ABS}. Union and intersection 
  are defined as modes rather than functions in accordance with the style of the early \texttt{GLIB} articles 
  and to leave this formalization extendable by graph decorators.\par
  To denote the graph family, a \texttt{Graph-yielding Function} from \cite{GLIB_000.ABS} could have been used. 
  But since sets of graphs would be needed sooner or later in the Mizar Mathematical Library \cite{BancerekJAR:2018} 
  (e.g. to count all spanning trees of a graph), the set attribute \texttt{Graph-membered} is rigorously introduced 
  in the first section.\par
  In the second section, the first condition of Wagner is formalized. It simply means that for two graphs 
  $G$ and $H$ from the family, their respective source and target function tolerate each other 
  ($S(G)\approx S(H)$ and $T(G)\approx T(H)$, cf. \cite{PARTFUN1.ABS}). As this property is indispensable 
  for unions (or else in a union an edge could point to different vertices), the set attribute was 
  named \texttt{\char`\\/-tolerating}. The graph union $U$ for a $\cup$-tolerating set $S$ is given by 
  \[U=\left({\textstyle \bigcup_{G\in S} V(G),\,\bigcup_{G\in S} E(G),\,\bigcup_{G\in S} S(G),\,\bigcup_{G\in S} T(G)}\right).\] 
  While Wagner's second condition is useful to ensure the resulting graph union will be non-multi, it is not 
  formalized in this article. A\par
  Since graphs without vertices are not allowed by the used definition \cite{GLIB_000.ABS}, the difference 
  between $\cup$-tolerating and \texttt{/\char`\\-tolerating} is the additional condition that  
  $\bigcap_{G\in S} V(G)$ is non empty. Then the graph intersection $I$ for a $\cap$-tolerating 
  set $S$ is given by 
  \[I=\left({\textstyle \bigcap_{G\in S} V(G),\,\bigcap_{G\in S} E(G),\,\bigcap_{G\in S} S(G),\,\bigcap_{G\in S} T(G)}\right).\] 
  To avoid confusion with intersection graphs of any kind, the mode was named \texttt{GraphMeet}.\par
  With this formalization the union of a graph with (any kind of) its complement will be complete and 
  the intersection will be edgeless, just as intended by \cite{GLIB_012.ABS}. }}

@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and 
  Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{GERWAG,
  title = {Graphentheorie},
  series = {B.I-Hochschultaschenbücher; 248},
  author = {Wagner, Klaus},
  address = {Mannheim [u.a.]},
  publisher = {Bibliograph. Inst.},
  year = {1970},
  ISBN = {3-411-00248-4},
  pages = {220 S.}
}
@book{SIMPLE,
  TITLE = {Introduction to graph theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver & Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}
@book{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate Texts in Mathematics; 244},
  AUTHOR = {Bondy, John Adrian; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ;
  http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; 
  http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}
@book{HANDBOOK,
  title = {Handbook of discrete and combinatorial mathematics},
  series = {Discrete mathematics and its applications},
  editor = {Rosen, Kenneth H. [Herausgeber]},
  address = {Boca Raton},
  publisher = {CRC Press},
  year = {[2018]},
  edition = {Second edition},
  ISBN = {978-1-58488-780-5},
  pages = {xxiv, 1590 Seiten},
},
}