@MISC{COUNTERS.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Extended Natural Numbers and Counters},
  SECTION1 = {Extended natural numbers},
  SECTION2 = {Sets of extended natural numbers},
  SECTION3 = {Relations with extended natural numbers in range},
  SECTION4 = {Ordinal preliminaries},
  SECTION5 = {Relations with cardinal domain},
  DAY = {25},
  MONTH = {October},
  YEAR = {2020},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {This article introduces extended natural numbers, 
  i.e. the set $\mathbb {N}\cup\{+\infty\}$, in Mizar and formalizes a way to list a 
  cardinal numbers of cardinals. Both concepts have applications in graph theory.},
  INTRODUCTION = {Extended natural numbers have often been used in the literature to   
  define distances in graphs that are not necessarily connected, to set the distance   
  between vertices of different components to $\+infty$, see e.g. \cite{MULTI,HOMO,AGT}.   
  Therefore it is only natural to formalize these numbers in preparation for a   
  formalization of distances in graphs. On the other hand, one usually does not see the   
  list of counters from the second part in the literature. The generalistic motivation   
  to introduce these is a rather simple one, however. $n$-partite finite graphs are   
  rather known and constructions like $K_{\omega,\omega}$ arise sometimes. 
  The index objects of these alone could be formalized using <tt>Cardinal-yielding XFinSequence</tt> 
  (cf. \cite{AFINSQ_1.ABS,CARD_3.ABS}, but a generalization for the   
  index object to be any cardinality long seemed to be appropriate. 
  This allows for easy notation of more graphs than just with the finite amount of indices. 
  For example $K_{1,2,3\ldots}$, where the index ranges over all natural numbers, 
  is an easy notation for a graph that does not have a finite independence number and also 
  no infinite subset of vertices that form an independet set.\par
  In the first section
  the set $\overline{\mathbb N}=\mathbb{N}\cup\{+\infty\}$ of extended natural numbers   
  is introduced to 
  the Mizar system \cite{FourDecades} as a subset of the extended real   
  numbers $\overline{\mathbb R}=\mathbb{R}\cup\{-\infty,+\infty\}$ defined in 
  \cite{NUMBERS.ABS}. Basic theorems will be proven, often specializations of 
  theorems from \cite{XXREAL_0.ABS,XXREAL_3.ABS} or generalizations of theorems 
  from \cite{NAT_1.ABS}. The second section will introduce sets of extended natural   
  numbers and proceed in a similar fashion to \cite{MEMBERED.ABS}. 
  The third section does the same with relations that only have extended natural numbers 
  in their range, similar to \cite{VALUED_0.ABS}. Section 4 deals with some ordinal 
  preliminaries. Not all are needed for the last section, but the author felt they would fit better 
  here than into a graph preliminary article. Finally, the last section introduces relations   
  with cardinal domain, as only a cardinal domain (in lieu of an ordinal one) is 
  needed   for counting purposes. The article ends with the definition of <tt>Counters</tt> and   
  <tt>Counters+</tt>, two expandable modes with the latter not allowing $0$ in its range.}}

@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{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{HOMO,
  title = {Graphs and homomorphisms},
  series = {Oxford lecture series in mathematics and its applications ; 28},
  author = {Hell, Pavol ; Nesetril, Jaroslav},
  address = {Oxford},
  publisher = {Oxford Univ. Press},
  year = {2004},
  ISBN = {0-19-852817-5},
  pages = {IX, 244 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}
}
@book{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}
}