# Order Extension and Szpilrajn's Extension Theorem

 Title: Order Extension and Szpilrajn's Extension Theorem Authors: Peter Zeller (p_zeller /at/ cs /dot/ uni-kl /dot/ de) and Lukas Stevens Submission date: 2019-07-27 Abstract: This entry is concerned with the principle of order extension, i.e. the extension of an order relation to a total order relation. To this end, we prove a more general version of Szpilrajn's extension theorem employing terminology from the book "Consistency, Choice, and Rationality" by Bossert and Suzumura. We also formalize theorem 2.7 of their book. Change history: [2021-03-22]: (by Lukas Stevens) generalise Szpilrajn's extension theorem and add material from the book "Consistency, Choice, and Rationality" BibTeX: @article{Szpilrajn-AFP, author = {Peter Zeller and Lukas Stevens}, title = {Order Extension and Szpilrajn's Extension Theorem}, journal = {Archive of Formal Proofs}, month = jul, year = 2019, note = {\url{https://isa-afp.org/entries/Szpilrajn.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Combinatorics_Words_Lyndon Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.