@MISC{GLIB_013.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Refined Finiteness and Degree properties in Graphs},
  SECTION1 = {Vertex- and edge-finite Graphs}
  SECTION2 = {Order and Size of a Graph as attributes},
  SECTION3 = {Locally finite Graphs},
  SECTION4 = {Degree properties in 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 finiteness of graphs is refined and the minimal and maximal 
  degree of graphs are formalized in the Mizar system \cite{FourDecades}, based on the formalization 
  of graphs in \cite{GLIB_000.ABS}.},
  INTRODUCTION = {The first section section introduces the attributes \texttt{vertex-finite} 
  and \texttt{edge-finite}, which are a refinement of \cite{GLIB_000.ABS}'s \texttt{finite}. 
  A notable result is the upper bound of the size of certain graphs in terms of their order, 
  e.g. that a simple finite graph with order $n$ and size $m$ satisfies $m\leq\binom{n}{2}$.\par
  Parametrized attributes for the order and size of a graph are introduced in the following section. 
  The main purpose of this additional notation (e.g. \texttt{G is n-vertex} instead of 
  \texttt{G.order() = n}) is to be used in clusterings and reservations in the future for 
  easy access, e.g. \texttt{reserve K2 for simple complete 2-vertex \_Graph}.\par
  The third section formalizes locally finite graphs, which are well known 
  (cf. \cite{DIEST,NASH,MULTI}).\par
  The minimal and maximal degree of a graph are usually defined, together with the degree of 
  a vertex, right at the beginning of general graph theory textbooks, often followed by the 
  Handshaking lemma (cf. \cite{MULTI,DIEST,SIMPLE,GERWAG}). While the Handshaking lemma is still 
  not proven in this article, the last section introduces the minimal and supremal degree of 
  a graph, the latter being called the maximal degree if a vertex attaining the supremal 
  degree exists. This doesn't always have to be the case, of course: Take for example the 
  sum of all complete graphs $\sum_{n=1}^\infty K_n$. Therefore the property of a graph having 
  a maximal degree is formalized, too. All formalizations are done as well for in/out degrees and 
  the relationship between them and the undirected degrees is taken into account.}}

@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}
}
@article{NASH,
  title={Infinite Graphs — A Survey},
  author={Nash-Williams, C. St. J. A.},
  journal={Journal of Combinatorial Theory},
  volume={3},
  number={3},
  pages={286--301},
  year={1967},
  publisher={Academic Press}
}
@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{DIEST,
  title = {Graph theory},
  series = {Graduate Texts in Mathematics; 173},
  author = {Diestel, Reinhard},
  address = {New York [u.a.]},
  publisher = {Springer},
  year = {2000},
  edition = {2. ed.},
  ISBN = {0-387-98976-5 ; 0-387-98976-5},
  pages = {XIV, 312 S.},
}
@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}
}