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
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.