@MISC{SCMYCIEL.MIZ,
  AUTHOR = {Rudnicki, Piotr and Stewart, Lorna},
  TITLE = {Simple Graphs as Simplicial Complexes:
     the {M}ycielskian of a Graph},
  NOTE = {This work has been partially supported by NSERC grant
      OGP 9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Simple Graphs as Simplicial Complexes},
  SECTION3 = {Induced Subgraphs},
  SECTION4 = {Clique, Clique Number, Clique Cover},
  SECTION5 = {Stable Set, Coloring},
  SECTION6 = {Mycielskian of a Graph},
  DAY = {7},
  MONTH = {February},
  YEAR = {2012},
  ADDRESS1 = {Department of Computing Science\\University of Alberta\\Edmonton, AB, Canada},
  ADDRESS2 = {Department of Computing Science\\University of Alberta\\Edmonton, AB, Canada},
  SUMMARY = {Harary~\cite[p.~7]{Harary69} claims
  that Veblen~\cite[p.~2]{Veblen31}
  first suggested to formalize simple graphs using simplicial complexes.
  We have developed basic terminology for simple graphs as
  as at most 1-dimensional complexes.\par
  We formalize this new setting and then reprove Mycielski's~\cite{Mycielski55}
  construction resulting in a triangle-free graph with
  arbitrarily large chromatic number. A different formalization
  of similar material is in~\cite{MYCIELSK.ABS}.}}

@book{Harary69,
  Author = {Frank Harary},
  Title = {Graph theory},
  Publisher = {Addison-Wesley},
  Year = {1969}
}

@book{Veblen31,
  Author = {Oswald Veblen},
  Title = {Analysis Situs},
  Publisher = {AMS Colloquium Publications},
  Volume={V},
  Year = {193}
}

@article{Mycielski55,
 author     = {J. Mycielski},
 title      = {Sur le coloriage des graphes},
 journal    = {Colloquium Mathematicum},
 volume     = {3},
 year       = {1955},
 pages      = {161-162}}

@ARTICLE(MYCIELSK.ABS,
      AUTHOR  = {Rudnicki, Piotr and Stewart, Lorna},
      TITLE   = {{T}he {M}ycielskian of a Graph},
      JOURNAL = {Formalized Mathematics},
      YEAR    = {2011, doi: 10.2478/v10037-011-0005-6},
      VOLUME  = 19,
      PAGES   = {27--34},
      NUMBER  = {{\bf 1}})
