Order Extension and Szpilrajn's Extension Theorem

Peter Zeller 📧 and Lukas Stevens 🌐

July 27, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


March 22, 2021
(by Lukas Stevens) generalise Szpilrajn's extension theorem and add material from the book "Consistency, Choice, and Rationality"


Session Szpilrajn

Used by